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.
Moreover, let denote the set of all variables occurring in C.
Proof. By induction on C.
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 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.
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.