Axiomatic Semantics

Origin. Floyd (1967), Hoare (1969). Program meaning via assertions. Preconditions and postconditions. Proof rules for constructs. Foundation for program verification.

Models. {P} S {Q}: if P holds before S, Q holds after. Partial correctness: assumes termination. Total correctness: proves termination. Weakest precondition calculus.

Formalism.

Hoare triple: {P} S {Q} P: precondition S: statement Q: postcondition

Assignment axiom: {Q[e/x]} x := e {Q}

Sequence: {P} S₁ {R} {R} S₂ {Q} ───────────────────────── {P} S₁; S₂ {Q}

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

While loop: {I ∧ B} S {I} ───────────────────── {I} while B do S {I ∧ ¬B} I: loop invariant.

Consequence: P' ⇒ P {P} S {Q} Q ⇒ Q' ─────────────────────────────── {P'} S {Q'}

Weakest precondition: wp(S, Q) = weakest P such that {P} S {Q}. wp(x := e, Q) = Q[e/x] wp(S₁; S₂, Q) = wp(S₁, wp(S₂, Q))

Total correctness: [P] S [Q]: must also terminate. Loop variants: decrease with each iteration.

Symbols.

Symbol	Unicode	Name	Meaning
{P}	—	Precondition	Before state
{Q}	—	Postcondition	After state
wp	—	Weakest pre	Weakest precondition
I	—	Invariant	Loop invariant

Metatheory. The system is sound against the operational semantics: every derivable triple is valid, by induction on derivations, with the while rule justified by induction on the number of iterations. Completeness cannot be absolute, since validity of {true} skip {φ} already encodes truth in the standard model of arithmetic, which is not recursively enumerable. Cook (1978) gave the right statement: for the while-language, if the assertion language is expressive for the interpretation — meaning every weakest liberal precondition is definable by an assertion — then the Hoare system is complete relative to an oracle for valid assertions, so the only gap is arithmetic, not the proof rules. Expressiveness is a genuine hypothesis and can fail, and Wand exhibited an interpretation over which the system is incomplete for that reason. Dijkstra's predicate transformer gives the equivalent formulation: {P} S {Q} is valid iff P implies wp(S, Q), and wp is monotone and conjunctive over the deterministic constructs.

Applies to. Program verification. Design by contract. Verification conditions. Proof assistants. Static analysis.

Limitations. Relative completeness is the best available, and even that fails for richer languages: Clarke (1979) proved that no sound and relatively complete Hoare axiomatization exists for a language combining recursive procedures, procedures as parameters, static scope and global variables, so the incompleteness is in the language constructs, not the assertion logic. The assignment axiom is unsound in the presence of aliasing, since a write through a pointer can change a variable the substitution Q[e/x] does not mention; repairing this is what separation logic's frame rule does. The while rule takes the invariant as given, and no algorithm supplies it. Partial correctness asserts nothing when the program diverges, so termination needs a separate well-founded variant argument. For shared-state concurrency the rules are not compositional: Owicki–Gries demands a global interference-freedom check across all proof outlines, so proofs do not compose from proofs of the parts.