Relative completeness of the Hoare total correctness calculus

The natural question about the strength of the deduction system arises in this case, too. As in the case of partial correctness, it turns out that the completeness of the calculus has its limitations: there can be several reasons for the calculus to not be complete. Either, the assertions used in the consequence rules cannot be captured by a complete proof system, or not every set of states can be represented by formulas of the language used for describing the assertions and arithmetical expressions of correctness proofs, and , finally, the proof system is simply not powerful enough to form a complete deduction system. The same reasoning as in the case of partial correctness shows that the first two obstacles can indeed prevent the deduction system to be complete. By Gödel’s incompleteness theorem the difficulties raised on the axiomatisability of the underlying arithmetical language exist in this case, too. Moreover, we must find a bound function when applying the loop rule for total correctness, and we have to make sure that our language is powerful enough to express these functions as terms. If all these requirements are met, we can prove that the deduction system is strong enough to ensure relative completeness with respect to usual models of arithmetic. The definability of the weakest precondition is again of key importance in the proof. First of all, we mention without proof the expressiveness of the wp-calculus and define the notions necessary for the property.

Definition 65. Let Form be the set of formulas, and be an interpretation. We say that is expressive for Form, if, for every command C and every , there exists such that

Without proof we state the following theorem. As before, we set the interpretation as the standard interpretation of Peano arithmetic. The next theorem says that the standard interpretation of arithmetic is expressive for the given language of Hoare logic.

Theorem 66. Let be a while program, . Then there exists such that

The proof is very similar to that in the case of the wlp-calculus. The definability of sets of states represented by wlp-expressions were enough to prove relative completeness in the case of partial correctness. However, for total correctness, we need a little bit more: it is also necessary that the bound functions should be expressible in our arithmetical language. First of all, we define some approximation of the bound function for a while loop.

Definition 67. Let , and assume X is a variable not occurring in C. Let

Define a partial function such that and , if is defined for s. The while loop is called the extended loop of C.

Intuitively, the value iter(C,s) supplies us with the number of iterations needed for C to come to a halt when started from state s, provided does not diverge for s.

Definition 68. A set of arithmetical expressions is called expressive, if, for every while loop C, there is an expression t such that

whenever is defined for s.

Expressibility means the ability to represent the number of iterations needed for a loop in our language of arithmetic. Obviously, addition, multiplication and subtraction are not enough for this purpose. We assume that every partial function computable by a Turing machine is a part of our language, which guarantees expressibility. We can formulate now the result on the relative completeness of the total correctness calculus. We omit the superscripts from the denotation of the sets of states represented by formulas.

Theorem 69. Let be an interpretation, assume is expressive for Form and Com, where Form is the set of formulas of the underlying logical language. Let . Assume furthermore that the set of arithmetical expressions of the language is expressive. Then, for every and P, ,

Proof. The proof goes by induction on C. We discuss only the main ideas of the proof. In what follows, as an abuse of notation let denote the formula expressing itself, when C is a program and Q is an arithmetical formula. We concentrate only on the case of the while loop, since the other cases are almost identical to those in the proof of Theorem 50. Let , assume . By Lemma 64,

The induction hypothesis gives

By Lemma 52, we obtain

The assumption on the validity of implies that is always defined whenever . Then the expressiveness gives a t such that , if . Let z be a new variable. Then, by Lemma 60 and the fact that t strictly decreases by every iteration of C, we obtain

By the induction hypothesis, we obtain

Moreover, , since t is always nonnegative. Then the premisses of the while loop fulfil, hence we can assert

which proves our claim.