Soundness of the Hoare total correctness calculus

As by the semantics of the partial correctness calculus, we can define the meaning of terms and first order formulas for a fixed interpretation . As before, if P is a formula and is the underlying interpretation, then is the set of all states in which P is true in . We omit the superscript from .

Definition 58. Let and be sets of states. Then

where, for and , .

We demonstrate below some properties of the relation . Prior to this, we need a lemma which justifies the choice of z in the total correctness loop rule.

Definition 59. Let C be a while program, then

Moreover, let denote the set of all variables occurring in C.

Lemma 60.

  1. Let C be a program and s, be such that . Then for any .

  2. Assume for all . Then , if .

Proof. By induction on C.

Lemma 61.

  1. ,

  2. ,

  3. iff and for some ,

  4. iff and ,

  5. and and together imply ,

  6. and and for some and iff .

Proof.

  1. By Definition 16, .

  2. by Definition 16. Assume . Then, for , is trivially true, which gives the result.

  3. By Definition 16, iff iff . Let

    Then and .

    The other direction follows from the fact that and implies .

  4. . Assume and . Then implies , the case for is equally trivial. As to the other direction, if and , then and for some . This implies and, furthermore, . The case for is similar.

  5. From and the determinism of computation sequences it follows that , which implies, as in the proof of Theorem 28, . It is enough to prove that there is no infinite sequence of computation starting from , if . Let such that is minimal among the states s with this property. By Definition 12,

    By hypotheses and and the determinism of computation sequences, we have such that

    and holds. If , we are done. Otherwise and, by Lemma 60, contradicting the assumption on s.

Now we are in a position to define the meaning of a Hoare total correctness formula. Let be the standard interpretation of Peano arithmetic, as before.

Definition 62. Let P and Q be formulas of Peano arithmetic, let C be a program. Then the meaning of with respect to , denoted by , is the truth value of the expression . We may omit the superscript if it is clear from the context.

Let denote that is derivable in the total correctness calculus. In what follows, we prove the soundness of the total correctness calculus. Assume is the usual interpretation of Peano arithmetic.

Theorem 63. The Hoare calculus for total correctness of while programs is sound. In notation:

Proof. The statement follows from Lemma 61.

As a final remark, since we know now how to interpret total correctness formulas, we would relate the meaning of total correctness formulas to weakest preconditions of programs.

Lemma 64.