Total correctness of recursive procedures

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 t is an arithmetical expression and n is a variable not occurring in P, Q, C and t. Moreover, n is treated in the proof as a constant, which means n can 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 variable n in the previous definition. Let be a recursive program. Obviously, never halts. Assume we were allowed to quantify n with an existential quantifier in the premiss. Then we would obtain the following contradiction. Let the bound function t be X, if is our hypothesis in the adaptation rule . Then, if existential quantification of n is 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, though n being 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.

Example 90.

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.

Remark 91. A decomposition strategy also works in this case. For the statement it is enough to establish and then prove .