Axiomatic Semantics

Pioneered by C.A.R. Hoare

• The Syntax & Semantics of an Axiom
• The Axioms for Program Constructs
• The Rules of Consequence
• Advantage: Good for program correctness proofs
• Disadvantage: Hard to model aliasing, stack overflow, garbage collection, etc.