Introduction
Axiomatic semantics defines the meaning of a program through the properties it satisfies rather than how it executes. Instead of describing execution steps (operational) or assigning mathematical meanings (denotational), axiomatic semantics specifies what can be proven about a program using logical axioms and inference rules. This approach is particularly powerful for program verification and proving correctness properties.
This article explores Hoare logic, proof rules, and practical applications in formal verification.
Historical Context
Axiomatic semantics was pioneered by Tony Hoare in 1969 with his seminal paper “An Axiomatic Basis for Computer Programming.” Hoare logic, as it became known, provided a formal framework for reasoning about program correctness. This work laid the foundation for modern program verification and has influenced the development of formal methods throughout computer science.
Core Concepts
Hoare Triples
The fundamental concept in axiomatic semantics is the Hoare triple:
Notation: {P} s {Q}
Meaning: If precondition P holds before executing statement s, then postcondition Q holds after s terminates.
Components:
- P (Precondition): A logical assertion about the state before execution
- s (Statement): The program statement being verified
- Q (Postcondition): A logical assertion about the state after execution
Example:
{x = 5} y := x + 1 {y = 6}
This says: “If x equals 5 before the assignment, then y equals 6 after.”
Assertions
An assertion is a logical formula describing properties of the program state:
State: σ: Var → ℤ (assignment of values to variables)
Assertion: A predicate P(σ) that is either true or false for a given state
Examples:
x > 0 "x is positive"
x = y + 1 "x is one more than y"
x > 0 ∧ y > 0 "both x and y are positive"
∀i. 0 ≤ i < n → a[i] > 0 "all array elements are positive"
Validity and Satisfiability
Valid Hoare Triple: {P} s {Q} is valid if:
- For all states σ where P(σ) is true
- If executing s from σ terminates in state σ'
- Then Q(σ’) is true
Notation: ⊨ {P} s {Q}
Satisfiable: A Hoare triple is satisfiable if there exist states where it holds.
Proof Rules
Axiomatic semantics provides inference rules for proving Hoare triples.
Axiom: Skip
─────────────────
{P} skip {P}
Skip does nothing, so the postcondition equals the precondition.
Axiom: Assignment
─────────────────────────────
{P[x ↦ e]} x := e {P}
Where P[x ↦ e] means “substitute e for x in P”
Intuition: To prove that x := e establishes P, we need P to hold with e substituted for x before the assignment.
Example:
To prove: {?} x := 5 {x = 5}
We need: x = 5 with x replaced by 5, which is 5 = 5 (true)
So: {true} x := 5 {x = 5}
Rule: Sequence
{P} s₁ {Q} {Q} s₂ {R}
──────────────────────────
{P} s₁; s₂ {R}
The postcondition of s₁ becomes the precondition of s₂.
Example:
{x = 5} y := x + 1 {y = 6} {y = 6} z := y * 2 {z = 12}
─────────────────────────────────────────────────────────
{x = 5} y := x + 1; z := y * 2 {z = 12}
Rule: Conditional
{P ∧ b} s₁ {Q} {P ∧ ¬b} s₂ {Q}
──────────────────────────────────
{P} if b then s₁ else s₂ {Q}
Both branches must establish the same postcondition Q.
Example:
{x ≥ 0} if x > 0 then y := 1 else y := 0 {y ≥ 0}
Rule: While Loop
{I ∧ b} s {I}
──────────────────────────
{I} while b do s {I ∧ ¬b}
Where I is the loop invariant—a property that holds before and after each iteration.
Intuition:
- I holds before the loop
- If I and b hold, executing s maintains I
- When the loop exits (b is false), I and ¬b hold
Example: Proving while x > 0 do x := x - 1 terminates with x = 0
Invariant: I = (x ≥ 0)
Precondition: {x ≥ 0}
Loop body: {x ≥ 0 ∧ x > 0} x := x - 1 {x ≥ 0}
Postcondition: {x ≥ 0 ∧ ¬(x > 0)} = {x = 0}
Rule: Consequence (Weakening)
P' → P {P} s {Q} Q → Q'
──────────────────────────────
{P'} s {Q'}
We can strengthen the precondition or weaken the postcondition.
Intuition: If P’ implies P, and we can prove {P} s {Q}, then {P’} s {Q} also holds.
Example:
{x > 5} x := x + 1 {x > 5}
Since x > 10 → x > 5, we have:
{x > 10} x := x + 1 {x > 5}
Proof Techniques
Forward Reasoning
Start with precondition and derive postcondition:
{x = 5}
y := x + 1
{y = 6} (from assignment rule)
z := y * 2
{z = 12} (from assignment rule)
Backward Reasoning
Start with desired postcondition and work backward:
Goal: {?} x := 5; y := x + 1 {y = 6}
Working backward:
{?} x := 5 {?} y := x + 1 {y = 6}
For y := x + 1 to establish y = 6:
Need: x + 1 = 6, so x = 5
Precondition for y := x + 1: {x = 5}
For x := 5 to establish x = 5:
Precondition: {true}
Result: {true} x := 5; y := x + 1 {y = 6}
Loop Invariant Discovery
Finding the right loop invariant is crucial:
Strategy:
- Identify what should be true throughout
- Verify it holds initially
- Verify it’s maintained by loop body
- Verify it implies the desired postcondition
Example: Summing array elements
Program: sum := 0; i := 0; while i < n do (sum := sum + a[i]; i := i + 1)
Invariant: I = (sum = Σⱼ₌₀^(i-1) a[j] ∧ 0 ≤ i ≤ n)
Initially: sum = 0, i = 0, so I holds
Maintained: If I holds and i < n, after loop body:
sum' = sum + a[i] = Σⱼ₌₀^i a[j]
i' = i + 1
So I still holds
Exit: When i ≥ n, we have sum = Σⱼ₌₀^(n-1) a[j]
Practical Example: Proving Correctness
Program: Compute factorial
n := input
result := 1
i := 1
while i ≤ n do (
result := result * i
i := i + 1
)
Specification: {n ≥ 0} program {result = n!}
Proof:
{n ≥ 0}
result := 1
{result = 1 ∧ n ≥ 0}
i := 1
{result = 1 ∧ i = 1 ∧ n ≥ 0}
Loop invariant: I = (result = (i-1)! ∧ 1 ≤ i ≤ n+1)
{I}
while i ≤ n do (
{I ∧ i ≤ n}
result := result * i
{result = i! ∧ i ≤ n}
i := i + 1
{result = (i-1)! ∧ i ≤ n+1} (I maintained)
)
{I ∧ ¬(i ≤ n)}
{result = n! ∧ i = n+1}
{result = n!}
Advanced Topics
Partial vs Total Correctness
Partial Correctness: {P} s {Q}
- If s terminates, Q holds
- Doesn’t guarantee termination
Total Correctness: [P] s [Q]
- s terminates and Q holds
- Requires proving termination
Termination Proof: Use variant function (decreasing measure)
Concurrency
For concurrent programs, extend Hoare logic:
{P₁} s₁ {Q₁} {P₂} s₂ {Q₂}
─────────────────────────────
{P₁ ∧ P₂} s₁ ∥ s₂ {Q₁ ∧ Q₂}
Requires non-interference: s₁ and s₂ don’t interfere with each other’s variables.
Separation Logic
Extends Hoare logic for reasoning about heap-allocated data:
{P * R} s {Q * R}
Where * is the separating conjunction (P and Q hold on disjoint heap regions).
Glossary
Assertion: A logical formula describing program state properties
Axiomatic Semantics: Defining meaning through provable properties
Hoare Logic: Formal system for proving program correctness
Hoare Triple: {P} s {Q} - precondition, statement, postcondition
Invariant: A property that holds throughout execution
Loop Invariant: A property maintained by each loop iteration
Postcondition: Assertion that should hold after execution
Precondition: Assertion that should hold before execution
Proof Rule: Inference rule for deriving Hoare triples
Variant Function: Decreasing measure proving termination
Practice Problems
Problem 1: Prove {x = 5} y := x + 1; z := y * 2 {z = 12}
Solution:
{x = 5}
y := x + 1
{y = 6} (assignment rule: x + 1 = 6 when x = 5)
z := y * 2
{z = 12} (assignment rule: y * 2 = 12 when y = 6)
Problem 2: Find a loop invariant for while x > 0 do x := x - 1 starting with x = n.
Solution:
Invariant: I = (x ≥ 0)
Initially: x = n ≥ 0, so I holds
Maintained: If x ≥ 0 and x > 0, then x - 1 ≥ 0, so I maintained
Exit: When x ≤ 0, we have x = 0 (since x ≥ 0 from invariant)
Problem 3: Prove {true} x := 5 {x = 5}
Solution:
By assignment rule: {P[x ↦ 5]} x := 5 {P}
We want: {true} x := 5 {x = 5}
So P = (x = 5)
P[x ↦ 5] = (5 = 5) = true
Therefore: {true} x := 5 {x = 5}
Related Resources
- Hoare Logic: https://en.wikipedia.org/wiki/Hoare_logic
- Axiomatic Semantics: https://en.wikipedia.org/wiki/Axiomatic_semantics
- Program Verification: https://en.wikipedia.org/wiki/Program_verification
- Formal Methods: https://plato.stanford.edu/entries/formal-methods/
- Separation Logic: https://en.wikipedia.org/wiki/Separation_logic
- Temporal Logic: https://plato.stanford.edu/entries/logic-temporal/
- Formal Semantics: https://plato.stanford.edu/entries/formal-semantics/
- Theorem Proving: https://en.wikipedia.org/wiki/Automated_theorem_proving
- Model Checking: https://en.wikipedia.org/wiki/Model_checking
- Proof Assistants: https://en.wikipedia.org/wiki/Proof_assistant
- Coq Proof Assistant: https://coq.inria.fr/
- Isabelle Theorem Prover: https://isabelle.in.tum.de/
- Dafny Verification: https://dafny.org/
- Why3 Verification: http://why3.lri.fr/
- Frama-C Framework: https://frama-c.cea.fr/
Conclusion
Axiomatic semantics provides a powerful framework for proving program correctness through logical reasoning. By specifying what can be proven about a program rather than how it executes, axiomatic semantics enables rigorous verification of critical properties.
Hoare logic, with its elegant proof rules and intuitive reasoning about preconditions, postconditions, and invariants, has become the foundation for modern program verification tools and techniques. From simple sequential programs to concurrent systems and heap-allocated data, axiomatic semantics continues to evolve and provide essential tools for ensuring software correctness.
Understanding axiomatic semantics is essential for anyone involved in formal verification, program analysis, or the development of reliable software systems. It bridges the gap between informal correctness arguments and rigorous mathematical proofs, enabling the development of provably correct software.
Comments