Hoare Logic

Testing shows the presence of bugs, never their absence — run a program on a thousand inputs and the thousand-and-first can still crash it. To say a program is correct — for every input satisfying some assumption, it produces a result satisfying some requirement — you need a proof, and to prove things about programs you need a logic of programs. In 1969 Tony Hoare gave us exactly that: a handful of inference rules that let you reason about code the way you reason about theorems.

The whole edifice rests on one deceptively simple object, the Hoare triple, and a rule for each way of building a program. Master the rules and you can, in principle, verify any program built from assignment, sequencing, conditionals and loops.

The Hoare triple

A Hoare triple is written

\{P\}\; C \;\{Q\}

and read: "if the assertion P (the precondition) holds before running command C, then Q (the postcondition) holds after — provided C terminates." That last clause matters: plain Hoare logic proves partial correctness — if the program stops, the answer is right. Proving it actually stops is a separate job. A trivially true triple makes the point: \{P\}\; \texttt{while true do skip}\; \{Q\} holds for any Q, because the loop never ends and the postcondition is never put to the test.

P and Q are assertions — predicate-logic statements about the program's variables, like x > 0 or y = n!\; \wedge\; 0 \le k \le n.

The rules, one per language construct

Hoare logic is a proof system: axioms and inference rules, where a rule's premises sit above the line and its conclusion below. Build a proof by stacking them to match the shape of your program.

\{Q[x := E]\}\; x := E \;\{Q\}

To make Q true of x afterwards, require that Q was already true of the value being assigned beforehand. Read it backwards: take the postcondition and substitute E for x to get the precondition. Example: \{x + 1 > 0\}\; x := x + 1 \;\{x > 0\}. It looks reversed the first time, then never surprises you again.

A tiny proof, start to finish

Let's verify a two-line swap-free maximum: after it runs, m holds the larger of a and b. Formally we want \{\texttt{true}\}\;\ldots\;\{m = \max(a,b)\}.

let m: number; if (a >= b) { m = a; // branch assumes a >= b } else { m = b; // branch assumes a < b } // postcondition: m === Math.max(a, b)

Apply the conditional rule. In the then branch we assume a \ge b; the assignment axiom on m := a with postcondition m = \max(a,b) demands a = \max(a,b) beforehand — which follows from a \ge b by consequence. The else branch assumes a < b, and b = \max(a,b) follows likewise. Both branches land on m = \max(a,b), so the whole conditional does. Two applications of the assignment axiom, two of consequence, one of the conditional rule — and the program is proved, for every a and b at once, no testing required.

The tempting "forwards" version — "if P holds, then after x := E we have P with E plugged in" — is subtly broken when x already appears in E. Backwards substitution sidesteps this entirely: it asks what must be true of the expression now so that the property holds of the variable later, and the variable's old value simply never enters the picture. Hoare's genius was to notice the backwards form is both simpler and always correct. It is the seed of the weakest-precondition calculus, which turns this whole logic into a mechanical procedure.

The rule of consequence has a direction, and getting it backwards proves false things. You may strengthen a precondition (assume more than you need — safe) and weaken a postcondition (promise less than you achieved — also safe). Going the other way is a classic fallacy: from \{x > 5\}\,C\,\{x > 0\} you may not conclude \{x > 0\}\,C\,\{x > 0\} — that would be assuming less up front, which the proof never justified. Precondition arrows point in (P \Rightarrow P'), postcondition arrows point out (Q' \Rightarrow Q). Memorise the two directions; almost every bogus "verification" gets one of them wrong.