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 .

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

TofCis 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 subprogramTofCis preceded exactly one annotation, which is called . Additionally, if, for the partial correctness assertion , and, for some subprogramT, 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.

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

else

fi

od

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.