Previously, we discussed the issue of completeness—i.e., whether it is possible to derive every valid partial correctness specification using the axioms and rules of Hoare logic. Unfortunately, if treated as a pure deductive system, Hoare logic cannot be complete. To see why, consider the following partial correctness specifications: The first is valid if and only if the assertion is valid while the second is valid if and only if the command does not halt.
It turns out that the culprit is the CONSEQUENCE rule, which includes two premises about the validity of implications between the assertions involved. Proving those implications for our two examples would require proving arbitrary logical predicates and proving that arbitrary IMP programs terminate. By Gödel’s incompleteness theorem, we know that there is no consistent mathematical proof system that can do the former. Therefore, Hoare logic cannot be complete in that sense.
On the other hand, Hoare logic does enjoy this property:
Theorem. . implies .
This result, due to Cook (1974), is known as the relative completeness of Hoare logic. It says that Hoare logic is no more incomplete than the language of assertions—i.e., if we had an oracle that could decide the validity of assertions, then we could decide the validity of partial correctness specifications. In other words, for any valid Hoare triple, there exists a proof in Hoare logic--as long as you have some external way to decide the validity of the premises to the CONSEQUENCE rule.
Weakest Liberal Preconditions
Cook’s proof of relative completeness depends on the notion of weakest liberal preconditions. Given a command and a postcondition , the weakest liberal precondition is the weakest assertion such that is valid. Here, “weakest” means that any other valid precondition implies .
That is, most accurately describes input states for which either does not terminate or ends up
in a state satisfying .
Formally, an assertion is a weakest liberal precondition of and if: We write for the weakest liberal precondition of command 𝑐 and postcondition 𝑄. From left-to-right, the formula above states that is a valid precondition: . The right-to-left implication says it is the weakest valid precondition: if another assertion 𝑅 satisfies , then implies . It can be shown that weakest liberal preconditions are unique modulo equivalence.
We can calculate the weakest liberal precondition of a command as follows: The definition of is slightly more complicated—it encodes the weakest liberal precondition for each iteration of the loop. To give the intuition, first define the weakest liberal precondition for a loop that termintes in steps as follows: We can then express the weakest liberal precondition using an infinitary conjunction: See Winskel Chapter 7 for the details of how to encode the weakest liberal precondition for a while loop as an ordinary assertion.
To check that our definition is correct, we can prove (how?) that it yields a valid partial correctness specification:
Lemma 1. It is not hard to prove that it also yields a provable specification:
Lemma 2. Relative completeness follows by a simple argument:
Proof Sketch. Let be a command and let and be assertions such that the partial correctness specification is valid. By Lemma we have By Lemma we have . We conclude using the CONSEQUENCE rule.
