Proof outlines

In order to facilitate the presentation of proofs, we can give them in the form of proof outlines: in this case local invariants are attached to certain program points. For the sake of readability, we give the rules for constructing proof outlines in the forms of derivations, like this: with the meaning that if , are proof outlines, then is also a proof outline. Let denote the the proof outline assigned to the structure .

Definition 32.

where is obtained from by omitting zero or more annotations except for annotations of the form for some . Let be a proof outline. Then is called standard, if every subprogram T of C is preceded at least one annotation and, for any two consecutive annotations and , either or . This means in effect that in a standard proof outline every proper subprogram T of C is preceded exactly one annotation, which is called . Additionally, if, for the partial correctness assertion , and, for some subprogram T, holds, we omit and consider the remaining proof outline as standard.

The lemma below sheds light on the straightforward connection between proof outlines and partial correctness proofs ŕ la Hoare.

Lemma 33.

  1. Let hold as a proof outline. Then is provable by the rules obtained from Theorem 28.

  2. Assume is provable applying Theorem 28. Then there is a derivable standard proof outline .

In fact, there is also a close relation between proof outlines and compositional partial correctness proofs in Floyd– Naur style: the two methods are basically equivalent. The interested reader can find more details on the subject in [3]. We can put this relation on other words by saying that the precondition of a subprogram of C is assertion assigned to the label corresponding to the point of execution belonging to that subprogram.

Example 34. Let us take the program of Example 25. We give a proof by annotations of the partial correctness statement .



while do


    if then












Observe that in order to obtain a valid proof outline we have to ensure, by Point 6 of Definition 32, that for the consequent annotations the upper one implies the lower one. Thus we have to check the validity of the relations

All of them trivially hold in our standard interpretation.