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 (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.