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 .

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.LetCbe a while program, then

Moreover, let denote the set of all variables occurring in

C.

Proof.By induction onC.

Proof.

By Definition 16, .

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

By Definition 16, iff iff . Let

Then and .

The other direction follows from the fact that and implies .

. 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.

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

swith 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.LetPandQbe formulas of Peano arithmetic, letCbe 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.

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.