Hoare Logic¶
A compositional program logic that proves precondition–command–postcondition judgments by rules aligned with program constructs, using assertions and invariants to reduce global correctness to local proof obligations.
Core Idea¶
Hoare logic is a formal system for proving that imperative program commands satisfy assertions about their states. Its central judgment is the Hoare triple
where (P) is a precondition, (C) a command, and (Q) a postcondition. Under the ordinary partial-correctness reading, the triple means: if execution begins in a state satisfying (P), then every terminating execution of (C) ends in a state satisfying (Q). Termination is not promised. Under a total-correctness reading, the judgment additionally requires termination.
Scope of Application¶
The classical calculus handles sequential imperative programs. Extensions address procedures, recursion, pointers and heaps, objects, exceptions, nondeterminism, concurrency, probabilistic programs, hybrid systems, and program refinement. Separation logic, dynamic logic, rely–guarantee reasoning, and concurrent separation logics extend or reorganize the same verification problem but should not be collapsed into the unqualified classical identity.
Hoare-style reasoning underlies verification-condition generators, deductive verifiers, proof-carrying code, certified compilation, contract systems, and interactive theorem-prover developments. Tools may infer assertions, discharge arithmetic obligations automatically, or ask a human for invariants. Automation changes the workflow, not the logical identity.
Clarity¶
The assignment axiom is easiest to read backward. To guarantee (Q) after x := E, require (Q[E/x]) before the assignment. If the desired postcondition is (x=5) after x := y+1, the calculated precondition is (y+1=5). Confusing substitution direction is a common error.
Manages Complexity¶
Hoare logic replaces an enormous set of execution traces with modular assertions. A procedure contract can be used at each call without re-proving the body; an invariant summarizes arbitrarily many loop iterations; a sequence rule confines reasoning about each command to an interface assertion. The proof structure follows the program structure, localizing failures to specific obligations.
Abstract Reasoning¶
A standard verification workflow is:
- State the precondition and desired postcondition.
- Expand the program’s syntax tree.
- Apply syntax-directed rules backward to generate verification conditions.
- Invent or infer invariants at loops and recursion boundaries.
- Prove the resulting logical implications in the assertion theory.
- For total correctness, add a variant valued in a well-founded order and prove decrease.
- Recheck that the operational semantics and environmental assumptions match the implementation.
Knowledge Transfer¶
The contract-and-composition pattern transfers directly across imperative languages and verification tools: preconditions delimit admissible inputs, postconditions describe guaranteed outputs, and invariants bridge repetition. It also transfers to database transactions, API contracts, and protocol steps when those systems have precise state-transition semantics.
Transfer becomes analogy when “precondition” and “postcondition” are informal checklist labels without a state model or sound inference rules. Hoare logic’s force comes from the semantic link between derivation and execution, not from three-part prose formatting.
Relationships to Other Abstractions¶
Current abstraction Hoare Logic Domain-specific
Parents (1) — more general patterns this builds on
-
Hoare Logic is a kind of Formal System Prime
Formal System is the proposed immediate parent: Hoare logic has a symbolic language, well-formed judgments, axioms and inference rules, and mechanically checkable derivations.
Hierarchy paths (2) — routes to 2 parentless roots
- Hoare Logic → Formal System → Formalization → Representation → Abstraction
- Hoare Logic → Formal System → Formalization → Transformation → Function (Mapping)
Neighborhood in Abstraction Space¶
Hoare Logic sits in a sparse region of the domain-specific corpus (84th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Unclustered & Miscellaneous (1565 abstractions)
Nearest neighbors
- Conditioned Disjunction — 0.85
- Closed Preordered Set — 0.81
- Accessibility Relation — 0.80
- Formal Verification — 0.79
- Unity of the Proposition — 0.79
Computed from structural-signature embeddings · 2026-09-08