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.