The presence of recursive calls means another source of nontermination: it may happen that the program entangles into an infinite sequence of recursions. The easiest such example is:

Definition 86.([5]) procedure Diverge; begin diverge end; diverge

Of course, in most of the cases, nontermination is not so obvious. Consider the example below:

Definition 87.([5]) procedure D;begin

if X=0 then

skip

else

X:=X-1

D;

X:=X+2

fi; end;

The procedure *D* satisfies the specification .
We can observe that it even terminates when started from a value . If ,
then termination is immediate. Otherwise, assume and we know that *D*
terminates for all values . Then the assignment before the recursive call reduces the
value of *X*, and for the new value termination is established. Thus the program terminates for *X*, too.
The argument above can be formalized as a deduction rule, this is the recursion rule for total
correctness.

Definition 88.Let be a procedure, then

where

tis an arithmetical expression andnis a variable not occurring inP,Q,Candt. Moreover,nis treated in the proof as a constant, which meansncan neither be substituted for, nor can it be quantified by an existential quantifier.

Remark 89.Adopting the discussion of [1], we give a short justification of the necessity of the restrictions for the variablenin the previous definition. Let be a recursive program. Obviously, never halts. Assume we were allowed to quantifynwith an existential quantifier in the premiss. Then we would obtain the following contradiction. Let the bound functiontbeX, if is our hypothesis in the adaptation rule . Then, if existential quantification ofnis allowed, we acquire . But is equivalent to , from which, applying the consequence rule again, we obtain , which is impossible.On the other hand, let be given. Assume is substituted for

n. Then we obtain , and . The premiss in the former formula is equivalent to , from which, by the consequent rule, follows. Hence, thoughnbeing a variable, it must be treated as a constant in the course of the proof.

The Hoare calculus for the total correctness of recursive programs can be obtained if we substitute the recursion rule for the above recursion rule in the Hoare calculus for partial correctness of recursive programs with all the notations of the form replaced by the forms . We remark that soundness and relative completeness results similar to those in the case of while programs hold in this case, too. We end up this chapter with a proof of a total correctness specification for the recursive program of Example 87.

procedure D;

begin

if X=0 then

[ X=2n ]

skip

[ X=2n ]

else

X:=X-1

D;

X:=X+2

fi;

end;

The step needs to be established with the help of the adaptation rule. By the rule of adaptation, we have , which, together with the consequence rule applied with , gives the result.