Example II of Program Correctness (Cont.)

We do this in the following way. Given the loop while E do L od, suppose we find an assertion W such that the following three conditions are true:
  1. W and ( E > 0 ) → wp( L, W )
  2. W and ( E ≤ 0 ) → Q
  3. P → W 
 { n > 0 }
 i := n;   sum := 0;
 while  i  do
   sum := sum + i;
   i := i – 1
 od
 { sum = 1 + 2 + … + n }
Then if we know that the loop 
     while  E  do  L  od
terminates, we must have 
     W → wp( while E do L od, Q )
This is because
  1. Every time the loop executes, W continues to be true, by condition (a).

  2. When the loop terminates, condition (b) says Q must be true.

  3. Finally, condition (c) implies that W is the required approximation for wp(while …, Q)
An assertion W satisfying condition (a) is said to be a loop invariant for the loop while E do L od, since a repetition of the loop leaves W true. In general, loops have many invariants W, and to prove the correctness of a loop, it sometimes takes a little skill to find an appropriate W, namely, one that also satisfies conditions (b) and (c). In the case of our example program, however, a loop invariant is not too difficult to find: 
   W = ( sum = (i+1) + … + n and i ≥ 0 )
is an appropriate one.