Hoare Logic and Weakest Preconditions

Symptom

You changed a loop. It looks right. The tests pass. You are not confident.

The reason you are not confident is that the tests check a finite set of inputs and the loop runs on all of them. You know this. So you stare at the loop and try to convince yourself by simulating it in your head, which works for three iterations and then stops working.

The specific case that always defeats this: binary search. Six lines, and Bentley’s version in Programming Pearls was wrong for twenty years, as was the one in the JDK, where (low + high) / 2 overflowed for arrays above $2^{30}$ elements. Everyone reviewed it. Everyone tested it. Nobody had a way to state what the loop maintained, so nobody noticed the arithmetic did not maintain it.

What is missing is not more tests. It is a language for saying what a program does that is precise enough to check, and a calculus for reducing a claim about execution to a claim about logic.

Statement

The unit is the Hoare triple:

read: if $P$ holds and $C$ is executed and terminates, then $Q$ holds. This is partial correctness; termination is a separate obligation, and the total correctness form is written $[P]\ C\ [Q]$.

The axioms, which are the whole system:

The assignment axiom runs backwards, which surprises everyone once. To guarantee $x > 5$ after x := y + 1, you need $y + 1 > 5$ before. Substitute into the postcondition; do not push forward from the precondition.

Argument

Why backwards. Forward reasoning must invent an existential: after x := y + 1, the new $x$ equals the old $y$ plus one, and you must quantify over the old value. Backward substitution avoids this entirely, and $\text{wp}$ is therefore mechanical: a syntactic transformation of the postcondition, computable by a program with no search.

That is why verification condition generators work. Push the postcondition backwards through the program, collect the side conditions, and hand the resulting formulas to an SMT solver. Dafny, Why3, ESC/Java, and Viper all have this exact architecture, and the solver is doing the part Cook’s theorem calls the oracle.

Loops are the only hard part, and the difficulty is precisely locatable. The loop rule needs an invariant $I$: true before, preserved by each iteration, and strong enough that $I \wedge \neg b$ implies what you wanted. Everything else in the system is mechanical. Invariants cannot be inferred in general, and the reason is immediate: an invariant strong enough to prove a postcondition would decide properties Rice’s theorem (T011) says are undecidable, and a sufficiently strong invariant for while (true) encodes termination (T010).

Binary search, done properly. The invariant is: if the target is in the array at all, its index lies in $[lo, hi)$.

lo = 0; hi = n;
while (lo < hi) {
    mid = lo + (hi - lo) / 2;
    if (a[mid] < target) lo = mid + 1;
    else hi = mid;
}

Check the three obligations. Establishment: initially $[0, n)$ is the whole array, so the invariant holds trivially. Preservation: the array is sorted; if a[mid] < target then the target cannot be at any index $\le mid$, so moving $lo$ to $mid+1$ preserves it, and symmetrically for the other branch. Termination: the variant is $hi - lo$, a non-negative integer that strictly decreases, because $mid < hi$ always and $mid \ge lo$ always, so each branch shrinks the interval by at least one.

Now the JDK bug is visible. Writing mid = (lo + hi) / 2 computes a value that overflows to negative once $lo + hi > 2^{31} - 1$, which happens for arrays larger than $2^{30} = 1{,}073{,}741{,}824$ elements. The proof obligation $lo \le mid < hi$ then fails, and with it preservation. The form lo + (hi - lo) / 2 is not a style preference; it is what makes the obligation discharge, since $hi - lo$ is bounded by the array length and cannot overflow.

The variant is the termination half. Partial correctness with an infinite loop is vacuously satisfiable: ${P}\ \texttt{while true do skip}\ {\text{false}}$ is a valid triple. Total correctness requires exhibiting an expression that maps into a well-founded order and strictly decreases each iteration. For binary search, $hi - lo$ works and drops from $n$ to 0 in $\lceil \log_2 n\rceil$ steps, so a billion-element array terminates in 30 iterations.

What separation logic added, and why it mattered. Classical Hoare logic struggles with the heap, because assigning through a pointer may change any assertion mentioning any pointer that might alias it. O’Hearn and Reynolds added the separating conjunction $P * Q$, meaning $P$ and $Q$ hold on disjoint portions of the heap, and with it the frame rule: if ${P}\ C\ {Q}$ and $C$ does not modify $R$’s footprint, then ${P * R}\ C\ {Q * R}$. That makes reasoning local, so verifying a list operation does not require mentioning the rest of the heap. Facebook’s Infer is built on separation logic and runs on every diff at their scale, which is the industrial answer to whether this scales.

Forbids

Automatic invariant inference in general. Undecidable. Heuristics — Daikon’s dynamic inference, interpolation, abstract interpretation (T047), template-based synthesis — find many invariants and cannot find all.

Proving termination in general. The variant must be supplied, and no procedure produces one for arbitrary programs (T010).

Partial correctness implying anything about a non-terminating program. The triple is vacuous if $C$ diverges, which is why safety-critical work uses total correctness.

Verifying a program against a specification you have not written. The logic proves $C$ satisfies $Q$. If $Q$ is wrong or incomplete, the proof is worthless and the bug survives with a certificate attached.

Does not forbid

It does not mean verification is impractical. This is the misreading that keeps the technique in academia in people’s minds while it ships in industry. seL4 is a fully verified microkernel, roughly 10,000 lines of C with a machine-checked proof of functional correctness against its spec. CompCert is a verified C compiler. AWS uses Dafny and the s2n TLS implementation is formally verified; Amazon’s Zelkova reasons about IAM policies for every customer. These are deployed systems.

It does not require verifying everything. Verify the invariants that matter and test the rest. Liquid Haskell, JML, and Rust’s #[requires]-style contract crates let you annotate selectively, and this incremental adoption is how the technique enters real codebases.

It does not mean the assertions must be complete specifications. Even partial specs catch real bugs. assert statements are Hoare triples with a runtime check instead of a proof, and every assertion you have ever written is this system used informally.

It does not require an interactive proof assistant. Modern SMT solvers — Z3, CVC5 — discharge most verification conditions automatically. The interaction is in supplying invariants, not in constructing proofs step by step.

It does not conflict with testing. Verification proves the spec; testing checks the spec is the right one, and catches everything outside the model such as compiler bugs, hardware faults, and misunderstood requirements. The seL4 team tests as well as proves, and for reasons they state explicitly.

Boundary

• The assertion language must be expressive enough. Cook’s completeness is relative: it assumes an oracle for arithmetic validity, which by Gödel (T015) cannot be a decision procedure.
• Sequential and deterministic by default. Concurrency needs Owicki-Gries, rely-guarantee, or concurrent separation logic, each substantially heavier.
• The heap needs separation logic. Classical Hoare logic on pointer programs drowns in aliasing side conditions.
• The model must match the machine. A proof over mathematical integers says nothing about a program using 32-bit words, which is exactly the binary search bug. Verification tools model machine arithmetic for this reason.
• Specification is the bottleneck. Writing a correct, complete spec is often harder than writing the program, and is not automatable.

The habit worth taking even without any tool: for every loop you write, state the invariant and the variant in a comment. You will find the bugs while writing the invariant, which is the cheapest place to find them.

Read next