Total correctness of while programs

Exercise 19. Let

C = X:=1;

Y:=0;

while do

    X:=m*X;

    Y:=Y+1

od

Prove the validity of the total correctness assertion .

Solution. The proof of total correctness needs a different formulation of the while rules in the Hoare calculus compared to partial correctness proofs. As a first example we give the proof as a derivation tree for the total correctness formula . As a loop invariant we choose . Let us introduce the following labels.

First of all, we demonstrate the validity of .

Let D denote the proof tree obtained as above. Then

To apply the while rule for total correctness, we have to show that a quantity expressed by an arithmetical expression decreases at every execution of the while loop. In other words, we have to find a bound function t. For t we can choose . Then we have to prove for a new variable Z. The last premiss of the while rule, follows trivially.

If E denotes the above proof tree, then, taking into account we have

Taking all these into consideration, we can deduce by the while rule for total correctness. Furthermore,

and

which was to be proved.

Exercise 20. Let

C = Y:=((n+1)/2);

while do

    Y:=Y-1

od

Prove the validity of the total correctness assertion , where is defined as in Exercise 15.

Solution. Total correctness proofs enjoy a certain decomposition property: for a proof of , it is enough to prove and then verifying termination by showing . We are going to follow this path in the present case. The proof is again presented in the form of a derivation tree. Below, let stand for the while loop of C, and let be an invariant for the while loop.

Moreover,

In addition,

which is the partial correctness assertion desired. To verify total correctness, we have to prove termination yet. To this end, the provability of needs to be checked. As for the invariant of the while rule we can settle . Then the proof of is immediate. Let . Then

where the validity of follows from the fact that and together imply , by which follows. is straightforward.

Exercise 21. Let C be the program of Example 34 computing the greatest common divisor of a and b.

C = X:=a;

Y:=b;

while do

    if XY then

        X:=X-Y

    else

        Y:=Y-X

    fi

od

Verify the validity of , where denotes the greatest common divisor of a and b.

Solution. If we apply the decomposition rule, a proof outline showing is already given in Example 34. Thus, it remains to prove termination only by presenting a proof outline for . As for P, let us choose , and let . Then

X:=a;

Y:=b;

while do

    

    if XY then

        

        

        X:=X-Y

        

    else

        

        

        Y:=Y-X

        

    fi

    

od

The only interesting implications are

but they are straightforward arithmetical relations, too. The validity of immediately follows.

Exercise 22. Let

C = X:=n;

Y:=1;

Z:=1;

while X1 do

    X:=X-1;

    Y:=Y+2;

    Z:=Y+Z

od

Verify the total correctness assertion .

Solution. We apply the decomposition rule again. To start out with, we check the validity of . Let us choose as loop invariant.

X:=n;

Y:=1;

Z:=1;

while X1 do

    

    

    X:=X-1;

    

    Y:=Y+2;

    

    Z:=Y+Z

    

od

As usual, we have to check the validity of the implications formed by subsequent assertions of the proof. The only nontrivial one is

which follows by well-known arithmetical equalities. What is left is the proof of . As loop invariant we can choose and suffices as bound function. We omit the straightforward proof.

Exercise 23. Let be an alphabet. Assume a is a word over . Let

C = Z:=w;

Y:=a;

while Z do

    if f(Z)=f(Y) then

        skip

    else

        Y:=Yf(Z)

    fi;

    Z:=t(Z)

od;

Y:=t(Y)

The functions f and t on words are defined as before. Let be the function on words over such that is v with all the occurrences of the first character of u deleted from v, otherwise, if u is empty, . For example, . Prove .

Solution. We prove something more general: . From this, the original claim follows as a special case. In accordance with the decomposition rule we split the claim into two statements: and . We present valid proof outlines for both assertions. We deal with the partial correctness assertion first. As invariant, set . For the sake of readability, we have explicitly indicated word concatenations in the previous equality.

Z:=w;

Y:=a;

while Z do

    

    if f(Z)=f(Y) then

        

        

        skip

    

    else

        

        

        Y:=Yf(Z)

    

    fi;

    

    Z:=t(Z)

    

od;

Y:=t(Y)

The nontrivial implications are

the latter one hinging in the fact that implies .

It remains to check . It is enough to choose as loop invariant and as bound function. Then , where is the body of the loop, and follow easily.

Exercise 24. Let

C = Z:=w;

Y:=;

while Z do

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

        Y=Yf(Z)

    else

        skip

    fi;

    Z:=t(Z)

od

Verify the total correctness assertion , where removes a character from each character sequence of w consisting of the same symbols. For example, .

Solution. As before, we prove first the partial correctness assertion , then give a valid proof outline for the claim . For loop invariant, we settle .

C = Z:=w;

Y:=;

while Z do

    

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

        

        

        Y=Yf(Z)

        

    else

        

        

        skip

        

    fi;

    

    Z:=t(Z)

    

od

As usual, we have to verify the validity of the following relations:

For the justification of the implications it is enough to check the facts below:

They can be verified by induction on the length of u. What is left is to demonstrate . For bound function, we choose , and the loop invariant we define as . Then the necessary conditions for a valid proof outline are trivially satisfied.