We claim that the following program, which computes the sum of integers less than or equal to a positive integer n, is correct:
{ n > 0 }
i := n; sum := 0;
while i do
sum := sum + i;
i := i – 1
od
{ sum = 1 + 2 + … + n }
Again, a specification for a program C can be written as
{P} C {Q}
where P represents the set of conditions that are expected to hold at the beginning of a program and Q represents the set of conditions one wishes to have true after execution of the code C.
The problem is now that our semantics for while-statements is too difficult to use to prove correctness.
H0( while E do L od, Q )
= E ≤ 0 and Q
Hi+1( while E do L od, Q )
= E > 0 and wp( L, Hi( while E do L od, Q ) )
wp( while E do L od, Q )
= there exists an i such that Hi( while E do L od, Q )
To show that a while-statement is correct, we really do not need to derive completely its weakest precondition wp(while …, Q), but only an approximation, that is, some assertion W such that W → wp(while …, Q).
Then if we can show that P → W, we have also shown the correctness of {P} while … {Q}, since
( P → W ) and ( W → wp( while …, Q ) )
→ ( P → wp( while …, Q ) )