Assume C is a program with precondition and postcondition , respectively. We can prove the validity of by dissecting the proof into verifications for program components. This leads to the idea of a compositional correctness proof which consists of the following substeps. in what follows, stands for the truth value of the assertion .
The following formulation of the correctness condition for while-loops can also be useful.
, which trivially holds.
, which is true if and only if . But then is trivially contained in .
, by Definition 16. Consider the assertion . Then i is an appropriate choice for the intermediate assertion in the theorem.
, by Lemma 21. By induction on n, making use of , we can show that . This involves .
, and for some and ’: then
Proof of Lemma 29. () Assume first , which is equivalent to
Then , and . Moreover, by Equation 1.2, .
() Let as in the statement of the lemma. Then is equivalent to
We can deduce from the previous relation, by induction on n, that
Applying Equation 1.3, we obtain the result as follows:
Thus is proven.
The relations of Theorem 28 give a proof method for a compositional verification of partial correctness of while programs. Thus, we can make use of the statements of Theorem 28 as the proof rules and axioms of a formal, semantical proof of partial correctness. The following theorems are devoted to this idea, the first of which is a reformulation of Theorem 28.
The other direction is called semantical completeness.
Theorem 31. Let C be a program, , . Assume holds. Then we can obtain by subsequent applications of the points of Theorem 28 as axioms and proof rules.
We used the terminology semantic soundness and completeness in the sense of . That is, soundness and completeness is understood relative to the partial correctness definition of Definition 22. This means that partial correctness is defined without reference to a mathematical logical language: the set of states used here as pre- and postconditions are arbitrary subsets of . We will see in later chapters that this picture considerably changes if we allow only sets of states emerging as meanings of logical formulas.