Slide 11.7: Example I of program correctness (cont.)
Slide 11.9: Example II of program correctness (cont.)
Home

Example II of Program Correctness

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 ) )