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.

Version

v4 · 2026-09-19 · History

Domain-specific #

2005

Domain group

Applied Sciences & Engineering

Origin domain

Computer Science & Software Engineering

Subdomain

Axiomatic Semantics and Program Verification → Computer Science & Software Engineering

Aliases

Hoare calculus, Floyd–Hoare logic, Axiomatic program logic

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

\[ \{P\}\;C\;\{Q\}, \]

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.

How would you explain it like I'm…

Before-and-After Promises

Think of a recipe card that says: if you start with flour and eggs, and you finish the recipe, you will have a cake. Hoare Logic is a way to write promises like that about computer programs. It says what must be true before the program runs and what will be true after, if the program finishes. Then you can check the promise step by step.

Before-and-After Program Proofs

Hoare Logic is a way to prove that a computer program does what it should. You write a 'before' statement, the program, and an 'after' statement, like {x is 5} add 1 to x {x is 6}. This means: if the before statement is true and the program finishes, the after statement will be true. It doesn't promise the program will finish unless you ask for that stronger promise. Big programs are checked by proving small pieces and fitting the proofs together. For loops, you find something that stays true every time around the loop.

Precondition–Command–Postcondition Proofs

Hoare Logic is a formal system for proving facts about programs that change state step by step. Its basic statement is the Hoare triple {P} C {Q}: P is the precondition, C the command, Q the postcondition. In the usual partial-correctness reading, it says that if C starts in a state satisfying P, then any run that terminates ends in a state satisfying Q; it does not promise C will terminate. A total-correctness version also demands termination. Every command type (assignment, sequencing, if-then-else, loops) has a proof rule, so proofs are built from proofs of parts. Loops need an invariant, a condition preserved by each iteration.

 

Hoare Logic is a deductive system for verifying imperative programs against specifications written in an assertion language. Its judgments are Hoare triples {P} C {Q}. Under partial correctness, the triple holds if every terminating execution of C from a P-state ends in a Q-state; non-termination vacuously satisfies it. Total correctness strengthens this to require termination. The system is compositional and syntax-directed: there are rules for assignment, sequential composition, conditionals, and while-loops, plus a rule of consequence that lets you strengthen preconditions and weaken postconditions. Proving a loop requires supplying an invariant preserved by the body; for total correctness one also supplies a variant that decreases in a well-founded order. The effect is to convert operational behavior into logical proof obligations, and the framework extends to procedures and concurrency.

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:

1. State the precondition and desired postcondition.
2. Expand the program’s syntax tree.
3. Apply syntax-directed rules backward to generate verification conditions.
4. Invent or infer invariants at loops and recursion boundaries.
5. Prove the resulting logical implications in the assertion theory.
6. For total correctness, add a variant valued in a well-founded order and prove decrease.
7. 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) — outgoing typed relations

• Hoare Logic is a kind of Formal System Prime

  Formal System is the broader abstraction this entry instantiates: 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 → is a kind of Formal System → presupposes Formalization → presupposes Representation → presupposes Abstraction

Show alternative path (1)

Neighborhood in Abstraction Space

Hoare Logic sits in a sparse region of the domain-specific corpus (86^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Unclustered & Miscellaneous (2769 abstractions)

Nearest neighbors

• Conditioned Disjunction — 0.85
• Closed Preordered Set — 0.81
• Denying the Antecedent — 0.80
• Proof of correctness — 0.80
• Instruction Set Architecture — 0.80

Computed from structural-signature embeddings · 2026-10-25