Total correctness

So far we were concerned with proving partial correctness of programs with respect to given specifications. In this section we discuss how to prove termination for while programs. Obviously, only the loop rule needs to be modified as the only source of nontermination. The new loop rule is as follows.

Definition 55.

In the above rule t is an arithmetical expression and z is a new variable not occurring in , t, B or C.

We may as well write the loop rule for total correctness in the form of a proof outline. We resort to Definition 32 when defining proof outlines for total correctness proofs. The only change is the case of the while loop, which is described by the following formation rule.

As before, is the proof outline corresponding to C, and is a proof outline obtained from by deleting any number of annotations. The annotations with labels and cannot be removed from any proof outline. The standard proof outlines are defined similarly to the case of partial correctness. As an example, let us prove the correctness of the integer division program below.

Example 56. [1]. Let D be the program:

;

;

while do

    ;

    

od

Let

and let . We construct a proof outline demonstrating the correctness of the specification .

;

;

,

while do

    

    

    ;

    

    

    

od

In order to make it a valid proof outline, we have to prove and , where C is the body of the while loop and is a valid proof outline for it. Moreover, the relations , and need to be shown. But their validity is straightforward to check. The only task remaining os the construction of the proof outline .

;

Since the implication trivially holds, the proof outline above is a valid proof outline for . By this, the total correctness of D for the given specification is proved.

Remark 57. The verification of the total correctness formula can be split into two, possibly smaller tasks: the verification of and then the demonstration of . This method is called the decomposition method.