A proof system that says exactly what a program does. Wrap a command C between an assertion before and an assertion after — the triple {P} C {Q} — and the claim is checkable: run C from every state where P holds and confirm Q holds after. Over a finite state space that is not a hand-wave, it is exhaustive. Down the center, the terms go in, the verifier decides, the proven triple comes out. The blue team builds and defends it; the red team tries to break it.
source C. A. R. Hoare, An Axiomatic Basis for Computer Programming, Communications of the ACM 12(10):576–580 (1969) — doi:10.1145/363235.363259. Rendered, not quoted.
Validity is not memorized; it is derived by five rules over a tiny imperative language (assignment, sequence, if, while) with arithmetic mod 4. The state is a pair (x,y) ∈ {0,1,2,3}² — just 16 states.
Assignment ⊢ {Q[x:=e]} x:=e {Q}. Sequence {P}C₁{R},{R}C₂{Q} ⊢ {P}C₁;C₂{Q}. If both branches land in Q. While an invariant preserved by the body survives the loop. Consequence strengthens P / weakens Q.
Rule licensing the current triple:
A Hoare triple is a program keeping its promise: given P, it guarantees Q. Hoare took the-natural-deduction — inference rules that build proofs from proofs — and pointed it at imperative code, one rule per construct.
The precondition each rule demands is computed backward from Q: the weakest assertion that still guarantees it. That is the-weakest-precondition — Dijkstra's calculus, the next sphere. Each sphere is the next one's premise.
The blue team's live check: re-derive the assignment axiom over its whole family of assertions and expressions, and re-verify the loop rule — confirming every instance against exhaustive execution. If red flips a rule, this badge is where it shows.
A Hoare triple has three parts: a precondition P (what is assumed before), a command C (what runs), and a postcondition Q (what must hold after). Assertions are boolean facts about the state; commands are:
| form | reads |
|---|---|
| x := e | assign e to x |
| C₁ ; C₂ | do C₁, then C₂ |
| if b then C₁ else C₂ | branch on b |
| while b do C | repeat while b |
Partial correctness: if C halts from a P-state, Q holds. Over 16 states each program below halts — feed the triple into the panel.
k tunes the postcondition target so the verdict moves live.
The verdict is computed by running C from every P-state and testing Q — never looked up. The table below is that exhaustive check.
| P-state (x,y) | after C (x,y) | Q? |
|---|
What the machine produces, proven: the current triple decided over all 16 states, plus the standing facts the self-check nails on load — the assignment axiom holds for every Q and e in its family, the sequence rule composes, and the loop invariant (x+y)=k survives every iteration for all four k.
The blue team's witness (left) re-derives these live; the red team (right) tries to make them wrong.
And it is incomplete over full arithmetic: by Gödel there is no finite axiom set proving every true triple. Hoare logic is only relatively complete (Cook, 1978) — it assumes an oracle for the assertion theory. Finding loop invariants is itself undecidable. The system is a frame for proof, not an automatic prover.
"A proved triple means the program terminates." Cut. Partial correctness only — divergence makes any Q hold. Total correctness needs a ranking function proved to decrease.
"The assignment axiom substitutes forward: {P} x:=e {P[e/x]}." Cut. The sound rule substitutes backward into the postcondition: {Q[x:=e]} x:=e {Q}. The forward reading is exactly the tamper below.
"Any invariant that's preserved will do." Kept, corrected. It must be preserved and strong enough that I∧¬b implies the goal — the hard, undecidable art.
The red team's move: apply the assignment axiom with the substitution in the wrong direction — {Q} x:=e {Q[x:=e]} — to "derive" a false triple. The blue team's witness (window 7) runs the exhaustive state check and catches the violating state.
Flip the direction and the derived precondition is wrong: some pre-state runs C into a state where Q fails. The witness recomputes, finds it, and turns red. Nothing is faked; the attack is real and it is caught.