## Partial correctness in Hoare logic

Exercise 8. Let C be the program computing the greatest common divisor of a and b of Exercise 7. Prove the following partial correctness formula:

We adopt the notation of Exercise 7 concerning the labelling of C.

Solution. We present the proof in the Hoare partial correctness calculus, in linear style. As loop invariant we choose the formula .

Exercise 9. Let C be the program of Exercise 4. Construct a proof for the partial correctness formula

We make use of the labels defined for C in Exercise 4. Again, we give the proof in a linear form, for invariant we choose the formula .

Solution.

Exercise 10. Let

C = Z:=1;

while do

if odd(Y) then

Y:=Y-1; Z:=Z* X

else

Y:= Y div 2; X:=X* X

fi

od

We introduce the following labels.

We prove the partial correctness assertion by giving a correct proof outline for it. We introduce , as invariant.

Solution.

Z:=1;

while do

if odd(Y) then

Y:=Y-1;

Z:=Z* X

else

Y:= Y div 2;

X:=X*X

fi

od

Additionally, in order to ensure that we obtained a correct proof outline, we need to prove the relations

where, as usual, denotes the fact that the sets of states represented by P is a subset of the states where Q hold. All the above relations are trivial arithmetical facts.

Exercise 11. Let the base set of the underlying interpretation be words over an alphabet . Let

C = Y:=;

Z:=X;

while do

Y=f(Z)Y;

Z:=t(Z)

od,

where is the head, is the tail of a non-empty word X, otherwise both of them are the empty word. Let denote the reverse of w. We construct a correct proof outline for the partial correctness assertion . For this purpose, we use the invariant .

Solution.

Y:=;

Z:=X;

while do

Y=f(Z)Y;

Z:=t(Z)

od

In order to complete the proof, we have to prove the implications

but they are trivially valid.

Exercise 12. Let

C = Y:=;

Z:=X;

while do

if f(Z)=f(t(Z))

then Y=Yf(Z)

else

Y=Yf(Z)f(Z)

fi

Z:=t(Z)

od

Prove the correctness of the formula , where is obtained from w by incrementing by one the lengths of the character sequences consisting of the same character. For example, let , then . We apply as loop invariant the formula .

Solution.

Y:=;

Z:=X;

while do

if f(Z)=f(t(Z))

then Y=Yf(Z)

else

Y=Yf(Z)f(Z)

fi

Z:=t(Z)

od

To complete the proof we must prove the following implications:

Among these implications the first and the last one are trivial, though the precise verification of the second and third one would need a proof by induction on the lengths of the words involved. In such cases, we omit the rigorous proofs of the statements formulated in the interpretation, we just rely on our intuition to estimate whether a certain assertion in the

Exercise 13. Let

C = Y:=;

Z:=X;

while do

if f(Y)=f(Z)

then Z=t(Z)

else

Y=Yf(Z)

fi

od

Prove the correctness of the formula , where is obtained from w by substituting every sequence of identical elements by one specimen of that element. For example, let , then . The reverse operator is defined as before. We apply as loop invariant the formula .

Solution.

Y:=;

Z:=X;

while do

if f(Y)=f(Z) then

Z=t(Z)

else

Y=Yf(Z)

fi

od

The proof becomes complete if we check the validity of the implications below:

Exercise 14. Let

C = X:=1;

Y:=n;

while do

X:=X*Y;

Y:=Y-2

od

Prove the correctness of the formula , where

Solution. We give a proof in derivation tree form now. We choose as invariant. We construct the tree step by step, proceeding from the simpler to the more compound one. First of all, we prove , where is the body of the while loop.

Let denote the above proof tree. Then

is what we required. Applying the while rule, we acquire the proof tree that follows

If denotes the proof tree obtained as above and stands for the proof tree below

then

is the proof tree searched for. The reader may have the impression that presenting a proof in a deduction tree form might be impose a more exhaustive task on the person constructing the proof than a proof in linear style. It seems indeed that this is the case, that’s why we prefer proofs written in linear style or in the form of a proof outline. In what follows, proofs will be presented in linear form proofs or as proof outlines in most of the cases.

Exercise 15. Let

C = Y:=0;

while do

Y:=Y+1

od;

Y:=Y-1

Prove , where denotes the greatest integer not greater than r for a non-negative real number r.

Solution. We present the proof of the partial correctness assertion in the form of a proof outline, providing at the same time a detailed verification of the validity of the proof outline. Let us choose as loop invariant. Our first aim is to support with a valid proof outline the assertion .

Let

be labels for C, let us denote the proof outlines corresponding to the formula by for some formulas P, Q and command W . Thus, let stand for the proof outline obtained as the last row of the above derivation. Then we have

Denoting the last proof outline as , we acquire

which is what was desired.

Exercise 16. Let

C = Y:=0;

X:=1

while do

X:=2*X

Y:=Y+1

od;

Y:=Y-1

Prove the validity of .

Solution. We prove the partial correctness formula by presenting a valid proof outline for it. Let us choose as loop invariant. Let

be labels for C.

Let denote the proof outline obtained in the final line of the derivation tree. Then we have

and

where and . Finally, since yields , which is equivalent to , we have

which completes the proof.

Exercise 17. Let

C = X:=2;

Y:=1

while do

if Xn then

Y:=Y+1

else

skip

fi

X:=X+1

od;

Prove the validity of , where is the number of the divisors of n.

Solution. We present a valid proof outline for the demonstration of the partial correctness formula. Let denote the number of divisors of n less than m, that is,

We choose as an invariant for the while loop.

X:=2;

Y:=1

while do

if Xn then

Y:=Y+1

else

skip

fi

X:=X+1

od;

To complete the proof, it remains to justify the implications as follows.

All of the above relations represent straightforward arithmetical facts.

Exercise 18. Finding loop invariants is the non-trivial part of proving partial correctness. The next example illustrates a situation like this, where the loop invariant might need a little ingenuity to find. Let

C = X:=n;

P:=2;

Y:=0;

while do

if PX then

X:=X div P;

Y:=Y+1

else

P:=P+1

fi

od

Prove the validity of , where denotes the integer division of a by b, and is the number of the prime divisors of n with multiplicity.

Solution. We have to find a suitable invariant reflecting precisely the operation of the while loop. Let , where should denote the least proper divisor of m. Observe that is always prime. Then we can construct the following proof outline

X:=n;

P:=2;

Y:=0;

while do

if PX then

X:=X div P;

Y:=Y+1

else

P:=P+1

fi

od

Again, to complete the proof we have to check the validity of the implications below.

They are all straightforward arithmetical relations with the possible exception of the second and third ones, the justifications of which relies on the fact of P being the minimal proper divisor of n, which is just the minimal prime divisor of n. Hence, , if , and , if . All the other relations follow easily.