Proving Constraints

If the constraint we are interested in proving is a ``transitive'' property (if it holds for and and for and then it holds for and ) then we can use the following proof rule to show the constraint holds of any execution of the state machine:

where A is the set of actions and and are quantified and qualified as described above. Or, in English:

1. For each action ,
   • assume
     • holds in the pre-state,
     • holds in the pre/post-states, and
   • show
     • holds in the pre/post-states.
2. Conclude that holds of all pairs of states in all executions.

What's the rationale for this proof rule? First, again I care only about reachable states. Second, consider any execution of my state machine:

If I can show that holds over any pair of successive states, , i.e., every single state transition, then surely it holds over any pair of states, ( ), where i < j. To show that it holds in any pair of successive states, I need only consider every possible action, which is the only way I can get from to . For each action, I need to make sure that the conjunction of its pre- and post-condition predicates imply the constraint.