Axiomatic Semantics: Proving Program Properties

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:

1. Identify what should be true throughout
2. Verify it holds initially
3. Verify it’s maintained by loop body
4. 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.