An invariant is supposed to be true of every state of every execution of a state machine. You might ask is there a corresponding notion for state transitions? The answer is ``yes,'' though because it is not as commonly discussed in the literature, there is no common term for such a property. Some people might simply call it another kind of invariant, one over state transitions rather than states. To avoid confusion with state invariants, I'm going to call it a constraint. This word is not standard; also, others may use ``constraint'' to mean something different.
Consider any execution of a state machine:
A constraint is a predicate that is true in all pairs of states, and , in every execution, where follows , but need not immediately follow it ( does not have to be ).
The statement of a constraint, , in full generality looks like:
As for statements of invariants, we omit (because it's understood) the universal quantification over executions and states; the condition about and both being states in the execution; and the condition that precedes in the execution.
A constraint that holds for the Counter example is that its value always strictly increases:
s'(x) > s(x)
Does this constraint (appropriately restated) hold for SimpleCounter? BigCounter (careful!)? FatCounter? RandomCounter?