4.4 Invariants and Temporal Properties

In addition to specifications of single operations, it is often desirable to specify invariants and history properties that hold for the whole component. An invariant is a predicate restricting the set of possible states. Invariants must also be respected by additional operations added in future versions. Without explicit invariants in a component contract, client programmers tend to assume the strongest invariant derivable from the visible interface. This practice is dangerous, because added operations in a later version might violate this invariant and because supplemental operations might only be visible to other selected clients.

Temporal properties restrict the set of possible transitions. We might state that a counter is never decreased. As with invariants, additional operations must respect these properties. Again, it is not safe to assume that the set of traces will remain unchanged; hence, only explicitly stated temporal properties must be assumed.