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.

Symbol	Unicode	Name	Meaning
{P}	—	Precondition	Holds before
{Q}	—	Postcondition	Holds after
[P]	—	Total pre	Termination guaranteed
:=	—	Assignment	Variable update
;	—	Sequence	Sequential composition
skip	—	Skip	No operation
wp	—	Weakest precondition	Minimum requirement
⊢	U+22A2	Derives	Provable triple
→	U+2192	Implies	Logical implication

Metatheory. Soundness: if a triple is derivable, it holds. Relative completeness (Cook): if a triple is true, it's derivable assuming we can prove the required assertions. The assertion language must be expressive enough. Verification condition generation: transform triple derivation into logical formulas. Total correctness requires variant functions for termination.

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

Limitations. Manual proof requires loop invariants, which are hard to discover. Scaling to large programs is challenging. No direct handling of pointers, aliasing, concurrency (see separation logic). Assertions are first-order; some properties need richer languages. Partial correctness ignores termination. Relative completeness depends on the assertion language.