Slide 11.10: Example II of program correctness (cont.)
Slide 12.1: The lambda calculus
Home

Example II of Program Correctness (Cont.)
  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 }
Proving the Condition (b)
We must show that (W and i≤0) → (sum=1+…+n). But this is clear: 
   W and i ≤ 0
 = ( sum = (i+1) + … + n and i ≥ 0 and i ≤ 0 )
 = ( sum = (i+1) + … + n and i = 0 )
 = ( sum = 1 + … + n and i = 0 )

Proving the Condition (c)
It remains to show that conditions just prior to the execution of the loop imply the truth of W. We do this by showing that 
     n > 0 → wp( i:=n; sum:=0, W )
We have 
   wp( i:=n; sum:=0, W )
 = wp( i:=n, wp( sum:=0, sum=(i+1)+…+n and i≥0 ) )
 = wp( i:=n, 0=(i+1)+…+n and i≥0 )
 = ( 0 = (n+1)+…+n and n≥0 )
 = ( 0 = 0 and n ≥ 0 )
 = ( n ≥ 0 )
and of course n>0 → n≥0. In this computation we used the property that the sum=(i+1)+…+n with i≥n is 0. This is a general mathematical property: Empty sums are always assumed to be 0. We also note that this proof uncovered an additional property of our code: It works not only for n>0, but for n≥0 as well. This concludes our discussion of proofs of programs.