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. Soundness: derivable triples are valid. Relative completeness (Cook): complete modulo assertion language. Expressiveness of assertions matters.

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

Limitations. Finding invariants hard. Relative completeness only. Pointers/aliasing complex. Concurrency needs extensions.