next up previous
Next: Proving Constraints Up: No Title Previous: Metacomment

Constraints

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:

tex2html_wrap_inline588

A constraint is a predicate that is true in all pairs of states, tex2html_wrap_inline378 and tex2html_wrap_inline592 , in every execution, where tex2html_wrap_inline592 follows tex2html_wrap_inline378 , but need not immediately follow it ( tex2html_wrap_inline592 does not have to be tex2html_wrap_inline600 ).

The statement of a constraint, tex2html_wrap_inline602 , in full generality looks like:

tex2html_wrap_inline604

As for statements of invariants, we omit (because it's understood) the universal quantification over executions and states; the condition about tex2html_wrap_inline378 and tex2html_wrap_inline592 both being states in the execution; and the condition that tex2html_wrap_inline378 precedes tex2html_wrap_inline592 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?





Norman Papernick
Mon Mar 18 14:28:12 EST 1996