In the first part of this section we deal with partial correctness of recursive programs, then we will see some examples for proving total correctness in the presence of recursion.

begin

if X1 then

X:=X div 2;

F;

X:=X+1

else

X:=0

fi;

X:=n

F;

F

Prove the validity of , with the help of , where

Cis the recursive program and denotes the function .

Solution.First of all, we prove by applying the recursion rule. This amounts to verifying from the assumption , whereDis the body of the procedure. We present the proof in the form of a proof outline.procedure F;

begin

if X1 then

X:=X div 2;

F;

X:=X+1

else

X:=0

fi;

end;

We have to verify from the assumption by applying the adaptation rule. Let and . Then, on one hand, we have

on the other hand

which involves

by the consequence rule. Hence, by the recursion rule, we can assert .

Prior to proving , we have to make an observation. By Theorem 82, it follows that is without side effect with respect to the variables outside of . This implies for any assertion not containing variables from

C. With this in hand, we can formulate the following proof outline.

X:=n

F;

F

,

where, for the subsequent assertions, the upper one implies the lower one easily, taking into consideration together with the above remark.

procedure F;

begin

if X2 then

X:=X-3;

F;

X:=X+1

else

X:=0

fi

end;

X:=40;

F;

F;

F

Prove , where

Cis the main recursive program, provided .

Solution.We wish to apply the recursion rule first, to this end, by assuming we seek to prove , whereDis the body ofF. We give the proof in the form of a proof outline.procedure F;

begin

if X2 then

X:=X-3;

F;

X:=X+1

else

X:=0

fi

end;

We have to justify by the adaptation rule . Let and . Then we have

moreover,

which, by the consequence rule, yields

Now we are in a position to prove .

X:=40;

F;

F;

F

procedure F;

begin

if X Y then

X:=X-Y

F;

Y:=Y+Z

else

Y:=1

fi

end

be procedure

F, and letC = X:=5

Y:=3;

Z:=5;

F

be the recursive program. Prove with the help of , where denotes the integer part of the result of dividing

kbym.

Solution.For the sake of tractability, we apply the notation and . In order to verify , we assume the previous relation and demonstrate that holds, whereDis the body of procedureF.

procedure F;

begin

if X Y then

X:=X-Y

F;

Y:=Y+Z

else

Y:=1

fi

end

We have to check, by applying the adaptation rule, the deducibility of . Let and . Then and implies , by which, making use of the consequent rule, we conclude . Taking into account the fact that , we can deduce . Putting all these together, we obtain , as desired. Finally,

X:=5

Y:=3;

Z:=5;

F

,

where the justification of requires one more application of the adaptation rule.

procedure F;

begin

if 2X then

X:=X-1;

F;

Y:=Y+2;

Z:=Y+Z+1

else

Y:=2;

Z:=4

fi

end;

X:=n;

F;

X:=Z;

F

Demonstrate making use of , where

Cis the main recursive program.

Solution.By the rule of recursion for total correctness, in order to prove we have to infer from with an appropriately chosent, whereDis the body ofF. Let . Then

procedure F;

begin

if 2X then

X:=X-1;

F;

Y:=Y+2;

Z:=Y+Z+1

else

Y:=2;

Z:=4

fi

end

Let and . The adaptation rule yields , moreover, and together yield , which was to be proved. The recursion rule for total correctness can be applied only if the additional condition fulfills, but this is straightforward. Hence, by the recursion rule, . With this in hand

X:=n;

F;

X:=Z;

F

We also have made use of the fact that , thus, . By this, the proof is completed.