5.1 When proving the (partial) correctness of a loop, the invariant appears both as an assumption (on entering the loop) and as a goal. This means that it must be treated in two completely different ways. We illustrate these different treatments by working with a formula F of the form
(forall Q(X)) P1(X) and P2(X)where Q(X) is something like
1 < X < N. This formula is
really an abbreviation for an implication, of the form
(forall X) Q(X) implies P1(X) and P2(X).If P1 and P2 are both equations, then in assuming this formula, we introduce two conditional equations,
cq t1(X) = t1'(X) if 1 < X and X < N .
cq t2(X) = t2'(X) if 1 < X and X < N .
On the other hand, in trying to prove the formula, we would first eliminate
the quantifier, then eliminate the implication, and finally eliminate the
conjunction, so that the setup would be something like the following:
op x : Int .
eq 1 < x = true .
eq x < n = true .
red t1(x) == t1'(x).
red t2(x) == t2'(x).
Of course, things are more complex for an invariant, because of taking account
of the state, the precondition, etc.
It may help to relate the three criteria (in the Proof Rules for while loops, pages 95 and 104) to the three edges of the graph for a simple loop (something like Figure E.2 on page 218, but with just one loop), as follows: each of the three nodes of this diagram corresponds to a predicate (or assertion), and each of its three edges corresponds to an implication between those assertions that needs to be proved. The loop invariant corresponds to the central node of the diagram.