Hoare Logic

Origin. C.A.R. Hoare introduced the axiomatic approach to program correctness (1969). Building on Floyd's work on flowcharts (1967). Foundation for formal program verification. Extended by many: weakest preconditions (Dijkstra), refinement calculus, separation logic. Turing Award 1980.

Models. Partial correctness of programs. A Hoare triple {P} C {Q} means: if precondition P holds before executing command C, and C terminates, then postcondition Q holds after. Specifies what programs do without executing them. Axiomatic: derive triples from axioms and rules.

Formalism.

Hoare triples: {P} C {Q}

• P: precondition (assertion about initial state)
• C: command (program fragment)
• Q: postcondition (assertion about final state)

Partial correctness: If P holds and C terminates, then Q holds. Total correctness: C terminates whenever P holds, and Q holds after. Written [P] C [Q].

Axioms and rules:

Skip axiom: {P} skip {P}

Assignment axiom: {P[E/x]} x := E {P} Substitute E for x in postcondition to get precondition.

Sequence rule: {P} C₁ {Q} {Q} C₂ {R} ───────────────────────── {P} C₁; C₂ {R}

Conditional rule: {P ∧ B} C₁ {Q} {P ∧ ¬B} C₂ {Q} ─────────────────────────────────── {P} if B then C₁ else C₂ {Q}

While rule: {P ∧ B} C {P} ───────────────────────── {P} while B do C {P ∧ ¬B} P is the loop invariant.

Consequence rule: P' → P {P} C {Q} Q → Q' ────────────────────────────── {P'} C {Q'} Strengthen precondition, weaken postcondition.

Weakest precondition (Dijkstra): wp(C, Q) = weakest P such that {P} C {Q} Computes preconditions backwards through code.

Symbols.

Metatheory. The system is sound with respect to the operational semantics of the while-language: every derivable triple is true, proved by induction on derivations, with the while rule justified by induction on the number of iterations. It is not complete in the absolute sense and cannot be, since {P} C {false} is valid exactly when C diverges from every P-state, and non-termination is not recursively enumerable, so the valid triples are not r.e. and no effective proof system enumerates them. Cook (1978) supplied the correct statement: Hoare logic is complete relative to an oracle for validity in the assertion language, provided that language is expressive — that is, provided the strongest postcondition of each command is definable in it. Peano arithmetic over the standard model is expressive, so relative completeness applies to integer programs. Wand (1978) exhibited an interpretation that is not expressive and for which the system is genuinely incomplete. Clarke (1979) proved the negative result for richer languages: with recursive procedures passed as parameters, static scope, and global variables together, no sound and relatively complete Hoare axiomatization exists. Total correctness [P] C [Q] requires a variant mapping states into a well-founded order that strictly decreases each iteration.

Applies to. Program verification. Proving array algorithms, sorting, arithmetic. Safety-critical software. Verified compilers. Teaching formal methods. Foundation for modern verification tools.

Limitations. Completeness is only relative: the consequence rule appeals to an oracle for the assertion language, and when that language is arithmetic Gödel's theorem makes the oracle non-recursive, so the proof system never becomes an algorithm. The expressiveness hypothesis can fail outright, and then the incompleteness is real rather than relative. The assignment axiom {P[E/x]} x := E {P} is unsound for the heap, because [E] := F can change the value read through an alias E′ that P mentions; recovering soundness requires either explicit alias hypotheses or the separating conjunction. The rules are also unsound for shared-variable concurrency, since one thread can falsify another's invariant mid-proof. Partial correctness asserts nothing about divergence — {P} while true do skip {Q} is derivable for every P and Q. A triple relates one pre-state to one post-state, so hyperproperties such as noninterference, which quantify over pairs of executions, are not Hoare triples at all. Clarke's result bounds how far the axiomatization can be pushed: for procedure-rich ALGOL-like languages there is no sound and relatively complete system.

© 2026 Lingenic LLC