The wlp-calculus

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 .

Definition 43.

Lemma 44. iff .

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

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.

Lemma 46.

Proof. The proof goes by induction on C.

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

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

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

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

Lemma 47. is expressible.

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 . Assume B and C have only X as parameter, the treatment of the general case is similar. It is enough to find a formula P such 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, let Q denote 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 Q be . Then, obviously, . Moreover, by induction on i, we can convince ourselves that , this means .