So far everything we’ve done has been testing invariants: statements that must be true for all states in a behavior. In this chapter, we introduce temporal properties: statements about the behavior itself. Temporal properties considerably expand the kinds of things we can check, providing a range of techniques that few other tools can match. Some examples of temporal properties:
Does the algorithm always terminate?
Will all messages in the queue get processed?
If disrupted, will the system return to a stable state over time?
Is the database eventually consistent?
Temporal properties are very powerful but ...
