In the previous section we mentioned that there is a difference between using arbitrary sets of states in the partial correctness assertions or sets of states expressible with first order formulas. If we intend to prove the completeness of the Hoare calculus, we need the ability to express certain assertions by first order formulas. In general, we cannot hope that to every set of states we can assign a formula true at that set. Nevertheless, if we choose Peano arithmetic as our logical formalism, it is capable of describing sets of states the expressibility of which turn out to be sufficient for the completeness of the Hoare calculus. We define below a function , is called the weakest liberal precondition of with respect to .

Thus the weakest liberal precondition of with respect to is the set
of all states *s* which end up in after the execution of *C*. Observe that, for an *s*, being in
does not require termination of *C* at *s*. Hence the epithet
"liberal". The interpretation is expressive for the underlying logical language, if the set of formulas
is rich enough to capture the weakest liberal preconditions of truth sets of formulas. More
precisely:

Definition 45.LetFormbe the set of formulas, and be an interpretation. We say that is expressive forForm, if, for every commandCand every , there exists such that

In the remainder of the section we settle the interpretation as the standard interpretation of first order arithmetic, and the logical language as the language of Peano arithmetic. Hence, we omit the superscripts standing for the interpretation. We give a sketch of the proof of the expressibility of the usual arithmetical interpretation for arithmetical formulas, since it also sheds light on the properties of the weakest liberal precondition. For the sake of readability, we ignore the distinction between formulas and their truth sets in the argument below.

Proof.The proof goes by induction onC.

iff implies for every . But iff . By this, follows.

iff implies for every . We have iff , which entails, by the substitution lemma, .

iff implies for every . Assume is defined. By Definition 16, there exists such that and . Then , hence .

iff implies for every . By Definition 16, . Assume and . Then . Since, by assumption, , we have . Hence . The same argument applies for the case . Thus . The reverse direction can be proved in an analogous way.

Proof.We give a sketch of the proof. First of all, we have the following relations: iff and for every . By Lemma 21, there is a finite sequence such that , and for every and . AssumeBandChave onlyXas parameter, the treatment of the general case is similar. It is enough to find a formulaPsuch that

By Gödel’s predicate we can code finite sequences of numbers by first order formulas, thus the above description can be turned into a first order formula proving the expressibility of the while loop. The interested reader is referred to [3], or [11] for the missing details of the proof.

Expressibility in this sense will be of key importance in the next section when we treat the
relative completeness of Hoare’s partial correctness calculus. The weakest liberal precondition is
interesting in itself by Lemma 44. The next method will provide us an illustrative way
to approximate the weakest liberal precondition for a while loop. Though the result is not
presented as a first order formula, it is more applicable in a practical sense when one tries to
compute the value of the function . We introduce a notation for the termination of a
computation sequence. If *C* is a program, let denote the fact
that the computation sequence of the operational semantics terminates when started with
. In this case we may also say that is defined for *s*.
Moreover, let .
With an abuse of notation, we identify below first order formulas with the sets of states they
represent.

Lemma 48.Let be a program, letQdenote a set of states. Then can be approximated iteratively by the union of the following sets of states.Assume furthermore . Then

Proof.By Definition 51, iff implies for every . By Lemma 21, iff there are such that , and for every and . Let this property be denoted by .

Assume . If , then, by the determinism of the operational semantics, there exists with . Let be as above. The proof proceeds by induction on

n. If , then we have . Otherwise, since , by Lemma 21 and property , we can assert . By the induction hypothesis, for some . It follows , which, together with , yields the result.Assume , let . We prove the statement by induction on

j. If , then Lemma 21 immediately gives the result. Otherwise, let for some . By definition, . Let . Then property holds for some . Since , we also have . By induction hypothesis, , that is, . But, together with property , this implies , as desired.

Remark 49.Observe that in the proof above the assumption was used only in one direction. In fact

is valid without any restrictions. For the other direction, however, the assumption is needed, as the following example shows. Let . Let

Qbe . Then, obviously, . Moreover, by induction oni, we can convince ourselves that , this means .