Slide 11.10: Example II of program correctness (cont.)

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

Example II of Program Correctness (Cont.)

We show the conditions (a), (b), and (c) in turn.

W and ( E > 0 ) → wp( L, W )
W and ( E ≤ 0 ) → Q
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 (a)
We must show that

   W and i > 0 → wp( sum := sum + i;  i := i – 1, W )

where

   W = ( sum = (i+1) + … + n and i ≥ 0 )

First, we have

   wp( sum := sum + i; i := i – 1, W )
 = wp( sum := sum + i; i := i – 1,
         sum = (i+1) + … + n and i ≥ 0 )
 = wp( sum := sum + i,  wp( i := i – 1,
         sum = (i+1) + … + n and i ≥ 0 ) )
 = wp( sum := sum + i,
         sum = ((i–1) + 1) + … + n and i – 1 ≥ 0 )
 = wp( sum := sum + i, sum = i + … + n and i – 1 ≥ 0 )
 = ( sum + i = i + … + n and i – 1 ≥ 0 )
 = ( sum = (i+1) + … + n and i – 1 ≥ 0 )

Now (W and i>0) → (W and i–1≥0), since

   W and i > 0
 = ( sum = (i+1) + … + n and i ≥ 0 and i > 0 )
 = ( sum = (i+1) + … + n and i > 0 ) → ( W and i–1 ≥ 0 )

Thus, W is a loop invariant.