L8) Axiomatic Semantics

Proving a Program is Correct

A program that runs without visible errors is not necessarily correct. Only a mathematical proof can guarantee it. Axiomatic semantics provides the tools to achieve this.

Where does this article fit in?

In L5, we saw three ways to give meaning to a program:

Operational: “how it executes” — explored in L6
Denotational: “what mathematical function it computes” — explored in L7
Axiomatic: “what properties it guarantees” — this is the subject of this article

With L8, the semantic trilogy is complete. Each approach has its strengths: SOS (Structural Operational Semantics) describes the how, denotational semantics describes the what, and axiomatic semantics describes the why it is correct.

Why is it important?

Tests can show the presence of bugs, never their absence. A program can pass thousands of tests and still contain a subtle error that only manifests in a particular case. Space probes, braking systems, cryptographic protocols — in these fields, “it seems to work” is not enough.

Axiomatic semantics, based on Hoare logic, allows us to prove that a program is correct: that it does exactly what it is supposed to do, for all possible inputs, not just those we have tested. This approach gave rise to Design by Contract (Eiffel, Ada/SPARK), contracts integrated into modern languages, and program provers like Dafny or Frama-C (automatic code verification tools).

The idea in one sentence

Axiomatic semantics describes the meaning of a program by the logical properties it preserves: if certain conditions are true before execution, others will be true after.

Let’s explain step by step

Example 1: The coffee machine (revisited)

Let’s revisit the coffee machine from L5 to see how the axiomatic approach reasons about this system.

In operational semantics, we described the transitions:

(waiting, 0€) → (waiting, 1€) → (ready, 2€) → (dispensing, 0€)

In denotational semantics, we described the function:

dispenser(2€, coffee) = coffee

In axiomatic semantics, we describe what the system guarantees:

{money ≥ 2€ ∧ button = coffee}
  press
{coffee_dispensed = true ∧ money = 0€}

Deciphering:

{money ≥ 2€ ∧ button = coffee}: the precondition — what must be true before

press: the command — the action executed

{coffee_dispensed = true ∧ money = 0€}: the postcondition — what is guaranteed after

∧: logical conjunction (“and”)

Reading: “If the user has inserted at least 2 euros AND has pressed the coffee button, THEN the coffee will be dispensed AND the money counter will be reset to zero.”

We don’t say how the machine works (is it gears? a micro-controller?). We don’t say what function it computes. We only say: here is the contract — what is guaranteed if the input conditions are met.

This is exactly the spirit of axiomatic semantics: reasoning about specifications, not about implementation.

Hoare Triples

The central formalism of axiomatic semantics is the Hoare triple:

{P} C {Q}

What is a Hoare triple?

Invented by Tony Hoare in 1969, it is a notation that links three elements:

P (precondition): a logical assertion about the program state before execution

C (command): the instruction or program to be executed

Q (postcondition): a logical assertion about the program state after execution

The triple {P} C {Q} reads: “if P is true before executing C, and if C terminates, then Q is true after.”

Concrete examples:

{x = 5}  x := x + 1  {x = 6}

Reading: “If x is 5 before the assignment, then x is 6 after.”

{x > 0}  x := x * 2  {x > 0}

Reading: “If x is positive before, then x remains positive after multiplication by 2.”

{true}  x := 7  {x = 7}

Reading: “Whatever the initial state (the true precondition is always satisfied), after x := 7, x is 7.”

The {true} notation as a precondition:

The precondition true means “no condition required” — the triple is valid regardless of the starting state. It is the weakest possible precondition.

The Axioms and Rules of Hoare Logic

The power of Hoare logic lies in a small set of rules that allow us to build correctness proofs for complete programs, brick by brick.

Assignment Axiom

This is the most fundamental rule — and the most surprising at first glance:

─────────────────────────── (Assignment)
{Q[x / e]}  x := e  {Q}

Deciphering:

Q[x / e] (read “Q where x is replaced by e”): we take the postcondition Q and replace every occurrence of x with the expression e

No premise above the bar: it is an axiom (always true, without condition)

The rule reads “backwards”: we start from the postcondition Q and work our way back to the precondition

Why backwards? It’s counter-intuitive, but logical: to know what must be true before the assignment, we look at what we want after and “undo” the assignment.

Example:

We want to prove {???} x := x + 1 {x = 6}.

Let’s apply the axiom: the postcondition is x = 6, so the precondition is (x = 6)[x / (x+1)], which means we replace x with x + 1 in x = 6:

(x = 6)[x / (x + 1)] = (x + 1 = 6) = (x = 5)

Result:

─────────────────────────────── (Assignment)
{x = 5}  x := x + 1  {x = 6}

Intuitive check: if x is 5 before, and we add 1, then x is indeed 6 after. The axiom works.

Another example:

{???}  x := x * 2  {x > 0}

Q = (x > 0)
Q[x / (x * 2)] = (x * 2 > 0) = (x > 0)

─────────────────────────────── (Assignment)
{x > 0}  x := x * 2  {x > 0}

Here, the precondition and postcondition are identical: multiplying a positive number by 2 keeps it positive.

Sequence Rule

When chaining two instructions, we compose the proofs:

{P} c₁ {R}    {R} c₂ {Q}
────────────────────────── (Sequence)
    {P}  c₁ ; c₂  {Q}

Deciphering:

R is an intermediate assertion: the postcondition of c₁ and the precondition of c₂

The rule states: if c₁ transforms P into R, and c₂ transforms R into Q, then the sequence c₁;c₂ transforms P into Q

It is a composition of proofs, like chaining two links of a logical chain

Example:

Let’s prove {x = 0} x := x + 1 ; x := x * 3 {x = 3}:

Step 1 — Assignment Axiom for x := x * 3 with Q = (x = 3):
    Q[x / (x * 3)] = (x * 3 = 3) = (x = 1)
    Therefore: {x = 1}  x := x * 3  {x = 3}

Step 2 — Assignment Axiom for x := x + 1 with Q = (x = 1):
    Q[x / (x + 1)] = (x + 1 = 1) = (x = 0)
    Therefore: {x = 0}  x := x + 1  {x = 1}

Step 3 — Sequence Rule with R = (x = 1):

    {x = 0} x := x + 1 {x = 1}    {x = 1} x := x * 3 {x = 3}
    ───────────────────────────────��──────────────────────────── (Sequence)
                {x = 0}  x := x + 1 ; x := x * 3  {x = 3}

Observation: we work “from right to left” — we start with the last instruction and work our way back. This is the natural method with the assignment axiom.

If Rule

{P ∧ b} c₁ {Q}    {P ∧ ¬b} c₂ {Q}
────────────────────────────────────── (If)
  {P}  if b then c₁ else c₂  {Q}

Deciphering:

P ∧ b: precondition P is true AND condition b is true (we enter the then branch)

P ∧ ¬b: precondition P is true AND condition b is false (we enter the else branch)

¬b: negation of b (“b is false”)

Both branches must lead to the same postcondition Q

The rule states: no matter which branch is taken, we arrive at Q

Example:

Let’s prove {true} if x ≥ 0 then y := x else y := -x {y = |x|}:

Then branch (x ≥ 0):
    {true ∧ x ≥ 0} y := x {y = |x|}
    If x ≥ 0, then x = |x|, so y := x gives y = |x|  ✓

Else branch (x < 0):
    {true ∧ ¬(x ≥ 0)} y := -x {y = |x|}
    If x < 0, then -x = |x|, so y := -x gives y = |x|  ✓

    {true ∧ x ≥ 0} y := x {y = |x|}    {true ∧ x < 0} y := -x {y = |x|}
    ──────────────────────────────────────────────────────────────────────── (If)
            {true}  if x ≥ 0 then y := x else y := -x  {y = |x|}

This program correctly calculates the absolute value of x, and the proof formally confirms it.

While Rule and Loop Invariant

This is the most powerful rule — and the most difficult:

    {I ∧ b}  c  {I}
─────────────────────────── (While)
{I}  while b do c  {I ∧ ¬b}

Deciphering:

I is the loop invariant: a property that remains true at each iteration

The premise states: if the invariant I is true AND condition b is true, then after one iteration of c, the invariant I is still true

The conclusion states: if I is true initially, then upon exiting the loop (when b becomes false), we have I AND ¬b

Analogy: The invariant is like a tightrope walker on a wire. With each step (iteration), they may sway (the state changes), but they always remain on the wire (the invariant is preserved). When they stop (the loop terminates), we know they are still on the wire (I) and have reached the other side (¬b).

The invariant is the key. Finding the right invariant is often the most difficult part of a correctness proof. It is as much an art as a science.

Consequence Rule

This rule allows us to adjust preconditions and postconditions:

P' ⟹ P    {P} C {Q}    Q ⟹ Q'
──────────────────────────────── (Consequence)
         {P'} C {Q'}

Deciphering:

P' ⟹ P: P’ is stronger than P (P’ implies P) — we strengthen the precondition

Q ⟹ Q': Q implies Q’ — we weaken the postcondition

If we know that {P} C {Q}, and we have stronger conditions at the input or weaker guarantees at the output, the triple remains valid

Intuition: If a program is correct under certain conditions, it is a fortiori correct under more restrictive conditions (strengthened precondition) or with fewer guarantees (weakened postcondition).

Example:

We know that {x = 5} x := x + 1 {x = 6}.

However, x = 6 implies x > 0. By the consequence rule:

{x = 5} x := x + 1 {x = 6}    (x = 6) ⟹ (x > 0)
──────────────────────────────────────────────���────── (Consequence)
          {x = 5}  x := x + 1  {x > 0}

We have weakened the postcondition: instead of guaranteeing that x is exactly 6, we only guarantee that it is positive. This is less precise, but still correct.

Loop Invariants

What is a loop invariant?

A loop invariant is a logical property that is:

True before the first iteration (initialization)

Preserved by each iteration (conservation)

Useful at termination: combined with the termination condition, it yields the desired postcondition

It is the “red thread” that runs through all iterations and allows us to conclude that the result is correct.

Example: Sum of integers from 1 to n

Consider this program that calculates the sum 1 + 2 + … + n:

s := 0 ;
i := 1 ;
while i ≤ n do
    s := s + i ;
    i := i + 1

Desired postcondition: {s = n × (n + 1) / 2}

Finding the invariant:

The idea is that s always contains the sum of integers from 1 to i - 1. Formally:

I : s = (i - 1) × i / 2  ∧  1 ≤ i ≤ n + 1

How to find an invariant?

Some heuristics:

Look at the postcondition: the invariant is often a “partial version” of the final result

Replace a constant with a variable: in s = n(n+1)/2, replace n with the loop variable i - 1

Check boundary cases: is the invariant true at the beginning (i = 1, s = 0)? At the end (i = n + 1)?

Correctness proof:

1. Initialization: Before the loop, s = 0 and i = 1.

I = (0 = (1 - 1) × 1 / 2) ∧ (1 ≤ 1 ≤ n + 1)
  = (0 = 0) ∧ (1 ≤ 1 ≤ n + 1)
  = true  ✓  (assuming n ≥ 0)

2. Conservation: We assume I ∧ i ≤ n and execute the body:

Before:  s = (i - 1) × i / 2  ∧  i ≤ n
After s := s + i:  s_new = (i - 1) × i / 2 + i = i × (i + 1) / 2
After i := i + 1:  i_new = i + 1

Verification of I with the new values:
    s_new = (i_new - 1) × i_new / 2
    i × (i + 1) / 2 = ((i + 1) - 1) × (i + 1) / 2
    i × (i + 1) / 2 = i × (i + 1) / 2  ✓

3. Loop Termination: When the loop stops, ¬(i ≤ n), so i = n + 1 (because i increases by 1 at each iteration and i ≤ n + 1 by the invariant).

I ∧ ¬(i ≤ n):
    s = (i - 1) × i / 2  ∧  i = n + 1
    s = ((n + 1) - 1) × (n + 1) / 2
    s = n × (n + 1) / 2  ✓

The proof is complete: the program correctly calculates the sum of integers from 1 to n.

Partial vs. Total Correctness

So far, we have discussed partial correctness. There is an important distinction:

Partial Correctness	Total Correctness
Notation	`{P} C {Q}`
Meaning	If C terminates, then Q is true
Termination	Not guaranteed
Difficulty	Simpler

What is partial correctness?

The triple {P} C {Q} states: “If P is true initially AND if C eventually terminates, then Q will be true.” But it says nothing about termination. If C loops indefinitely, the triple is vacuously true (trivially true, because the condition “if C terminates” is never met).

Example: {true} while true do skip {false} is a valid partial correctness triple. Since the loop never terminates, the postcondition false is never reached, and the triple is never violated.

What is total correctness?

The triple [P] C [Q] (with square brackets instead of curly braces) states: “If P is true, then C terminates AND Q is true afterwards.” This is a stronger guarantee: we prove both that the result is correct AND that the computation terminates.

Proving Termination: Loop Variants

To move from partial correctness to total correctness, we must prove termination. The main tool is the variant (or termination function).

What is a loop variant?

A variant is an integer-valued expression that:

Is positive (or zero) at each iteration

Strictly decreases at each iteration

Since an integer cannot decrease indefinitely while remaining positive, the loop must terminate.

Example: For the sum loop, the variant is n + 1 - i:

Before the loop: n + 1 - 1 = n ≥ 0 (if n ≥ 0) ✓
At each iteration: i increases by 1, so n + 1 - i decreases by 1 ✓
When the variant reaches 0: i = n + 1, the condition i ≤ n is false, the loop stops ✓

Invariant vs. variant:

Invariant: what does not change (preserved property) — proves correctness

Variant: what changes (quantity that decreases) — proves termination

Both together give total correctness

Application to BP3

What could be axiomatically proven about a BP3 grammar?

Grammar Termination:

In BP3, a grammar can loop indefinitely if a rule is recursive without a termination condition:

RND[1]
gram#1[1] S --> do4 S
gram#1[2] S --> do4

In axiomatic semantics, we could formulate:

{weight(gram#1[1]) = w ∧ w > 0}
  derive(S)
{number_of_derivations ≤ f(w)}

With decremental weights (<50-12>), the variant would be the sum of the weights of the recursive rules: it decreases with each application until it reaches zero, forcing termination.

Musical Properties:

We could express musical invariants:

{tessitura ⊆ [C3, C6]}
  derive_complete(Grammar)
{∀ note ∈ result : C3 ≤ note ≤ C6}

“If all terminal notes of the grammar are within the tessitura [C3, C6], then the result will remain within this tessitura.”

Why this is the least used semantics for BP3:

No classic loops: BP3 uses recursive rewriting, not while loops. The assignment axiom does not apply directly.
Stochasticity (probabilistic nature of the derivation process): classic Hoare logic is deterministic. Proving properties about a random process requires probabilistic extensions (probabilistic Hoare logics).
Complexity: axiomatic proofs for stochastic grammars with decremental weights would be very cumbersome.

Operational semantics (L6) remains the most natural tool for BP3. For a detailed exploration, see the B1.

Comparative Table of the Three Semantics

Criterion	Operational (SOS)	Denotational	Axiomatic (Hoare)
Question	How does it execute?	What function does it compute?	What does it guarantee?
Formalism	Transition rules	Functions on domains	Pre/postconditions
Notation	`⟨e, σ⟩ ⟹ ⟨e', σ'⟩`	`e : D → D'`	`{P} C {Q}`
Strengths	Close to code, executable	Compositional, abstract	Correctness proofs
Weaknesses	Verbose, low-level	Difficult for effects	Manual annotations
Ideal for	Interpreters, debuggers	Optimization, equivalence	Verification, contracts
Handles stochasticity	Naturally (via probabilities)	Via probabilistic monads	Extensions needed
Handles mutable state	Naturally (via configurations)	Via state monads	Naturally (via assertions)
For BP3	Primary choice (SOS)	Possible but complex	Limited (no classic loops)

Modern Formal Verification Tools

Hoare logic remained a theoretical tool for a long time. Since the 2000s, practical tools have made formal verification accessible.

Interactive Provers:

Coq (France, INRIA): theorem prover based on type theory. Used to certify the CompCert compiler (formally verified C compiler), mathematical foundations (four-color theorem), and cryptographic protocols
Isabelle/HOL (Cambridge/Munich): general-purpose prover used in the verification of operating systems (seL4, formally verified microkernel) and protocols
Lean (Microsoft Research): recent prover, very active in the mathematical community (Mathlib project)

Language-Integrated Verification:

SPARK/Ada: a subset of Ada with contracts (preconditions, postconditions, invariants) statically verified. Used in aeronautics, railways, and defense
Dafny (Microsoft Research): language with automatic verification. Invariants are written, Dafny automatically proves correctness
Eiffel: pioneer of Design by Contract (Bertrand Meyer, 1986). Preconditions (require), postconditions (ensure), and class invariants (invariant) are integrated into the language

Design by Contract:

Bertrand Meyer’s idea is to apply Hoare triples directly in the code:

-- Example in Eiffel (simplified syntax)
withdraw (amount : INTEGER)
    require
        amount > 0
        balance >= amount
    do
        balance := balance - amount
    ensure
        balance = old balance - amount
        balance >= 0
    end

This style has been adopted (in various forms) by Java (@Contract), Python (assert), Kotlin (require/ensure), and many others.

A Bit of History

Robert Floyd (1967) laid the foundations with his method of “intermediate assertions” on flowcharts. The idea: annotate each point of a program with a logical assertion and verify that transitions preserve these assertions. Floyd was the first to formalize the notion of a loop invariant.

C.A.R. Hoare (1969) published “An Axiomatic Basis for Computer Programming” in Communications of the ACM. He distilled Floyd’s ideas into an elegant deductive system: the triples {P} C {Q} and a small set of rules (assignment, sequence, if, while, consequence). The article, remarkably concise (12 pages), is one of the most cited in computer science.

Edsger Dijkstra (1975-1976) reversed the perspective with the calculation of weakest preconditions. Instead of asking “is this precondition sufficient?”, he asked “what is the weakest precondition that guarantees this postcondition?”. The notation wp(C, Q) gives the weakest precondition P such that {P} C {Q}. His book A Discipline of Programming (1976) systematized this approach and profoundly influenced software engineering.

wp and Hoare logic:

Dijkstra’s wp calculus is, in a way, the “mechanized” version of Hoare logic. For the assignment axiom, wp(x := e, Q) = Q[x / e] — exactly Hoare’s rule, but formulated as an automatic calculation rather than a manual deduction. This calculation is the basis of modern automatic verifiers like Dafny.

Key Takeaways

Hoare Triple {P} C {Q}: if P is true before and C terminates, then Q is true after. This is the central formalism of axiomatic semantics.
Assignment Axiom: we “work backwards” from the postcondition to the precondition by substituting the variable. {Q[x/e]} x := e {Q}.
Loop Invariant: a property preserved at each iteration. Finding the right invariant is the core of the proof.
Loop Variant: a quantity that strictly decreases at each iteration, guaranteeing termination.
Partial vs. Total Correctness: {P} C {Q} does not guarantee termination; [P] C [Q] guarantees it.
Consequence Rule: allows strengthening preconditions and weakening postconditions.
For BP3: axiomatic semantics is the least direct (no classic loops, stochasticity), but the concepts of invariant and termination remain relevant for reasoning about grammars.

Glossary

Weakening: replacing a postcondition with a weaker condition (less precise but still correct). If x = 6 is true, then x > 0 is also true: we have weakened the postcondition.
Assertion: a logical property about the program state at a given point. Preconditions and postconditions are assertions.
Axiom: a rule without premises, always applicable. The assignment axiom is the only axiom in Hoare logic.
Partial Correctness: property {P} C {Q} — if C terminates, Q is true. Says nothing about termination.
Total Correctness: property [P] C [Q] — C terminates AND Q is true. Combines partial correctness and termination.
Design by Contract: a programming methodology where functions are annotated with preconditions, postconditions, and invariants. Invented by Bertrand Meyer (Eiffel, 1986).
Loop Invariant: a logical property true before the loop and preserved by each iteration. Key to proving loop correctness.
Class Invariant: a property that must be true for any object of a class, at any observable time (between method calls).
Hoare Logic: a formal system of triples {P} C {Q} and inference rules for proving program correctness. Introduced by C.A.R. Hoare in 1969.
Weakest Precondition (wp): the least restrictive condition P such that {P} C {Q} is valid. Notation: wp(C, Q). Introduced by Dijkstra (1975).
Postcondition: an assertion describing what is guaranteed after the execution of a command. Noted Q in {P} C {Q}.
Precondition: an assertion describing what must be true before the execution of a command. Noted P in {P} C {Q}.
Strengthening: replacing a precondition with a stronger (more restrictive) condition. If we know that {x > 0} C {Q}, then {x = 5} C {Q} is also valid because x = 5 implies x > 0.
Substitution Q[x / e]: an operation that replaces every occurrence of the variable x with the expression e in the formula Q. Example: (x > 3)[x / (x + 1)] = (x + 1 > 3) = (x > 2).
Hoare Triple: notation {P} C {Q} that links a precondition P, a command C, and a postcondition Q. Reads “if P is true before C, and if C terminates, then Q is true after”.
Variant (termination function): a positive integer expression that strictly decreases at each iteration of a loop. Its existence proves termination.
Formal Verification: the use of mathematical methods to prove that a system (software or hardware) satisfies its specification.
∧ (conjunction): logical connector “and”. P ∧ Q is true if and only if P and Q are both true.
¬ (negation): logical connector “not”. ¬P is true if and only if P is false.
⟹ (implication): logical connector “implies”. P ⟹ Q means “if P is true, then Q is true”.

Prerequisites: L5
Reading time: 12 min
Tags: #axiomatic-semantics #hoare-logic #verification #program-proof

Previous article: L7
L series completed. For application to BP3, see: B1

L8) Axiomatic Semantics

Proving a Program is Correct

Where does this article fit in?

Why is it important?

The idea in one sentence

Let’s explain step by step

Example 1: The coffee machine (revisited)

Hoare Triples

The Axioms and Rules of Hoare Logic

Assignment Axiom

Sequence Rule

If Rule

While Rule and Loop Invariant

Consequence Rule

Loop Invariants

Example: Sum of integers from 1 to n

Partial vs. Total Correctness

Proving Termination: Loop Variants

Application to BP3

Comparative Table of the Three Semantics

Modern Formal Verification Tools

A Bit of History

Key Takeaways

Further Reading

Glossary