Hoare Logic

Hoare logic is a formal system for reasoning about the correctness of imperative programs, developed by Tony Hoare in 1969. It provides a deductive calculus for proving that a program satisfies its specification by relating the program's preconditions and postconditions to its commands. The central construct is the Hoare triple: {P} C {Q}, which states that if the program state satisfies the precondition P before executing command C, then the state will satisfy the postcondition Q after C terminates.

The logic is compositional: the correctness of a compound program is derived from the correctness of its parts. The rule for sequential composition states that if {P} C₁ {R} and {R} C₂ {Q}, then {P} C₁; C₂ {Q}. This modularity allows proofs to scale with program structure, matching the structure of the code itself. The logic also includes rules for assignment, conditionals, and loops — the latter through the loop invariant, a property that holds before and after each iteration and that implies the desired postcondition when the loop terminates.

Hoare logic was the first practical formal method for program verification and remains the foundation of most modern program logics. It has been extended to concurrent programs (Owicki-Gries logic), object-oriented programs, and programs with pointers and heap structures (separation logic). The predicate transformer semantics of Dijkstra's weakest preconditions provide an alternative formulation that is equivalent in expressive power but often more convenient for automated reasoning.

The practical impact of Hoare logic has been limited by the undecidability of the general correctness problem: there is no algorithm that can decide whether an arbitrary program satisfies an arbitrary specification. Hoare logic provides a proof system, but constructing proofs requires human insight or heuristic automation. The development of SMT solvers and program verifiers like Dafny and Why3 has brought automated Hoare-style reasoning to real programs, though the gap between research tools and industrial practice remains substantial.

Hoare logic is often presented as the ancestor of modern verification — respected but superseded. This is the wrong framing. Hoare logic is not a historical waypoint on the path to model checking and theorem proving. It is the enduring grammar of imperative reasoning. Every program verifier that checks a loop invariant, every static analyzer that tracks program state, every debugger that asks 'what must be true here' is speaking Hoare logic, whether it knows it or not. The notation has changed, but the logic has not.