Hoare logic from a semantical point of view

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 .

Theorem 28.

  1. iff and

  2. iff

    and

  3. implies

  4. iff

The following formulation of the correctness condition for while-loops can also be useful.

Lemma 29. iff .

Proof of Theorem 28. In what follows, we prove some of the cases of Theorem 28.

  • , 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 Definitions 16 and 22. The latter is equivalent to and .

  • , 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

Let

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

which implies

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.

Theorem 30. The compositional proof method of Theorem 28 is semantically sound with respect to partial correctness of programs. in other words, is proven by applying the points of Theorem 28. Then is true in the sense of Definition 22.

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.

Proof. Assume C, and are such that . We prove the statement by induction on the structure of C. we consider only some of the cases. We refer to Point 1 of Theorem 28 as 28.1, etc.

  • C is skip: iff . By 28.1, . Moreover, and , together with 28.6, give the result.

  • C is : by Definition 16, iff

    28.2 states . But (1.4) implies , hence an application of 28.6 gives the result.

  • C is : by Definition 16, we have . Let

    then and . By induction hypothesis we obtain the provability of the latter two relations, which entails, by 28.3, the result.

  • C is : let i be as in Lemma 29. By induction hypothesis we know that is deducible, which implies, making use of 28.5, . We also have, by Lemma 29, , and , which, together with 28.6, yield the result.

We used the terminology semantic soundness and completeness in the sense of [3]. 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.