Axiomatic Semantics · roomi fields

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 the what, and axiomatic the why it is correct.

Why Is This 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 domains, “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 that have been tested. This approach gave rise to Design by Contract (Eiffel, Ada/SPARK), integrated contracts in 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 afterwards.

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:

(attente, 0€) → (attente, 1€) → (prêt, 2€) → (distribution, 0€)

In denotational semantics, we described the function:

[[distributeur]](2€, café) = café

In axiomatic semantics, we describe what the system guarantees:

$\{\text{argent} \geq 2€ \;\wedge\; \text{bouton} = \text{café}\} \quad \text{appuyer} \quad \{\text{café\_distribué} = \text{vrai} \;\wedge\; \text{argent} = 0€\}$

Deciphering:

$\{\text{argent} \geq 2€ \;\wedge\; \text{bouton} = \text{café}\}$ : the precondition — what must be true before

$\text{appuyer}$ : the command — the action executed

$\{\text{café\_distribué} = \text{vrai} \;\wedge\; \text{argent} = 0€\}$ : the postcondition — what is guaranteed after

$\wedge$ : 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 microcontroller?). 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 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 \times 2 \;\{x > 0\}$

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

$\{\text{vrai}\}\; x := 7 \;\{x = 7\}$

Reading: “Regardless of the initial state (the precondition $\text{vrai}$ is always satisfied), after $x := 7$ , $x$ is $7$ .”

The notation $\{\text{vrai}\}$ as a precondition: The precondition $\text{vrai}$ (or $\text{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 building correctness proofs for complete programs, brick by brick.

Assignment Axiom

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

$\dfrac{}{\{Q[x/e]\}\; x := e \;\{Q\}} \quad \text{[Affectation]}$

Rule 1 — Assignment Axiom: no premise above the bar (it’s an axiom). The precondition is obtained by substitution into the postcondition.

Deciphering:

$Q[x/e]$ (read ” $Q$ where $x$ is replaced by $e$ ”): we take the postcondition $Q$ and replace each 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:

$\dfrac{}{\{x = 5\}\; x := x + 1 \;\{x = 6\}} \quad \text{[Affectation]}$

If $x = 5$ before, then $x = 6$ after $x := x + 1$ .

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

Another example:

$\{?\!?\!?\}\; x := x \times 2 \;\{x > 0\}$

$Q = (x > 0)$ , so $Q[x / (x \times 2)] = (x \times 2 > 0) = (x > 0)$

$\dfrac{}{\{x > 0\}\; x := x \times 2 \;\{x > 0\}} \quad \text{[Affectation]}$

Multiplying a positive number by 2 keeps it positive.

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:

$\dfrac{\{P\}\; c_1 \;\{R\} \qquad \{R\}\; c_2 \;\{Q\}}{\{P\}\; c_1;\,c_2 \;\{Q\}} \quad \text{[Séquence]}$

Rule 2 — Sequence: composition of two proofs via an intermediate assertion $R$ .

Deciphering:

$R$ is an intermediate assertion: the postcondition of $c_1$ and the precondition of $c_2$

The rule states: if $c_1$ transforms $P$ into $R$ , and $c_2$ transforms $R$ into $Q$ , then the sequence $c_1;\,c_2$ transforms $P$ into $Q$

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

Example:

Let’s prove $\{x = 0\}\; x := x + 1 ;\; x := x \times 3 \;\{x = 3\}$ :

Step 1 — Assignment Axiom for $x := x \times 3$ with $Q = (x = 3)$ :

$Q[x / (x \times 3)] = (x \times 3 = 3) = (x = 1) \quad \Rightarrow \quad \{x = 1\}\; x := x \times 3 \;\{x = 3\}$

Step 2 — Assignment Axiom for $x := x + 1$ with $Q = (x = 1)$ :

$Q[x / (x + 1)] = (x + 1 = 1) = (x = 0) \quad \Rightarrow \quad \{x = 0\}\; x := x + 1 \;\{x = 1\}$

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

$\dfrac{\dfrac{}{\{x = 0\}\; x := x + 1 \;\{x = 1\}} \text{[Aff]} \qquad \dfrac{}{\{x = 1\}\; x := x \times 3 \;\{x = 3\}} \text{[Aff]}}{\{x = 0\}\; x := x + 1;\, x := x \times 3 \;\{x = 3\}} \quad \text{[Séquence]}$

Complete proof tree: two assignment axioms (at the top) composed by the sequence rule (at the bottom).

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

If Rule

$\dfrac{\{P \wedge b\}\; c_1 \;\{Q\} \qquad \{P \wedge \neg b\}\; c_2 \;\{Q\}}{\{P\}\; \mathbf{if}\; b \;\mathbf{then}\; c_1 \;\mathbf{else}\; c_2 \;\{Q\}} \quad \text{[If]}$

Rule 3 — If: both branches must lead to the same postcondition $Q$ .

Deciphering:

$P \wedge b$ : precondition $P$ is true AND condition $b$ is true (we enter the then branch)

$P \wedge \lnot b$ : precondition $P$ is true AND condition $b$ is false (we enter the else branch)

$\lnot 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 $\{\text{vrai}\}\; \mathbf{if}\; x \geq 0 \;\mathbf{then}\; y := x \;\mathbf{else}\; y := -x \;\{y = |x|\}$ :

Then branch ( $x \geq 0$ ): $\{\text{vrai} \wedge x \geq 0\}\; y := x \;\{y = |x|\}$ If $x \geq 0$ , then $x = |x|$ , so $y := x$ yields $y = |x|$ .

Else branch ( $x < 0$ ): $\{\text{vrai} \wedge \lnot(x \geq 0)\}\; y := -x \;\{y = |x|\}$ If $x < 0$ , then $-x = |x|$ , so $y := -x$ yields $y = |x|$ .

$\dfrac{\{\text{vrai} \wedge x \geq 0\}\; y := x \;\{y = |x|\} \qquad \{\text{vrai} \wedge x < 0\}\; y := -x \;\{y = |x|\}}{\{\text{vrai}\}\; \mathbf{if}\; x \geq 0 \;\mathbf{then}\; y := x \;\mathbf{else}\; y := -x \;\{y = |x|\}} \quad \text{[If]}$

Absolute value proof: both branches guarantee $y = |x|$ .

This program correctly computes 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:

$\dfrac{\{I \wedge b\}\; c \;\{I\}}{\{I\}\; \mathbf{while}\; b \;\mathbf{do}\; c \;\{I \wedge \neg b\}} \quad \text{[While]}$

Rule 4 — While: the invariant $I$ is preserved at each iteration, and the negation of $b$ is acquired upon exit.

Deciphering:

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

The premise states: if invariant $I$ is true AND condition $b$ is true, then after one iteration of $c$ , 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 \wedge \lnot 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 ( $\lnot 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 adjusting preconditions and postconditions:

$\dfrac{P' \Rightarrow P \qquad \{P\}\; C \;\{Q\} \qquad Q \Rightarrow Q'}{\{P'\}\; C \;\{Q'\}} \quad \text{[Conséquence]}$

Rule 5 — Consequence: strengthening the precondition and weakening the postcondition.

Deciphering:

$P' \Longrightarrow P$ : $P'$ is stronger than $P$ ( $P'$ implies $P$ ) — we strengthen the precondition

$Q \Longrightarrow Q'$ : $Q$ implies $Q'$ — we weaken the postcondition

If we know that $\{P\}\; C \;\{Q\}$ , and we have stronger input conditions or weaker output guarantees, 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 weaker guarantees (weakened postcondition).

Example:

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

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

$\dfrac{\{x = 5\}\; x := x + 1 \;\{x = 6\} \qquad (x = 6) \Rightarrow (x > 0)}{\{x = 5\}\; x := x + 1 \;\{x > 0\}} \quad \text{[Conséquence]}$

Weakening of the postcondition: from $x = 6$ (precise) to $x > 0$ (weaker but correct).

We have weakened the postcondition: instead of guaranteeing that $x$ is exactly $6$ , we only guarantee that it is positive. It 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 upon exit: combined with the termination condition, it yields the desired postcondition

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

Example: Sum of Integers from 1 to n

Consider this program that calculates the sum $1 + 2 + \ldots + n$ :

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

Desired postcondition: $\{s = n \times (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 = \frac{(i - 1) \times i}{2} \;\wedge\; 1 \leq i \leq 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$ )?

Proof of correctness:

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

$I = \left(0 = \frac{(1 - 1) \times 1}{2}\right) \wedge (1 \leq 1 \leq n + 1) = (0 = 0) \wedge (1 \leq 1 \leq n + 1) = \text{vrai} \quad (n \geq 0)$

2. Conservation: We assume $I \wedge i \leq n$ and execute the body:

Before: $s = (i - 1) \times i / 2 \;\wedge\; i \leq n$
After $s := s + i$ : $s_{\text{new}} = (i - 1) \times i / 2 + i = i \times (i + 1) / 2$
After $i := i + 1$ : $i_{\text{new}} = i + 1$

Verification of $I$ with the new values:

$s_{\text{new}} = \frac{(i_{\text{new}} - 1) \times i_{\text{new}}}{2} \;\Leftrightarrow\; \frac{i \times (i + 1)}{2} = \frac{((i + 1) - 1) \times (i + 1)}{2} = \frac{i \times (i + 1)}{2} \quad \checkmark$

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

$I \wedge \lnot(i \leq n) :\quad s = \frac{(i - 1) \times i}{2} \;\wedge\; i = n + 1 \quad\Rightarrow\quad s = \frac{n \times (n + 1)}{2} \quad \checkmark$

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

Partial Correctness vs Total Correctness

Up to this point, we have discussed partial correctness. There is an important distinction:

	Partial Correctness	Total Correctness
Notation	$\{P\}\; C \;\{Q\}$	$[P]\; C \;[Q]$
Meaning	If C terminates, then Q is true	C terminates AND Q is true
Termination	Not guaranteed	Guaranteed
Difficulty	Simpler	More difficult

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: $\{\text{vrai}\}\; \mathbf{while}\;\text{true}\;\mathbf{do}\;\text{skip} \;\{\text{faux}\}$ is a valid partial correctness triple. Since the loop never terminates, the postcondition $\text{faux}$ 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, termination must be proven. 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 strictly 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 \geq 0$ (if $n \geq 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 \leq 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 yield 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, one could formulate:

$\{\text{poids}(\text{gram\#1}[1]) = w \;\wedge\; w > 0\} \quad \text{dériver}(S) \quad \{\text{nombre\_dérivations} \leq 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:

One could express musical invariants:

$\{\text{tessiture} \subseteq [\text{do3}, \text{do6}]\} \quad \text{dériver\_complet}(\text{Grammaire}) \quad \{\forall\, \text{note} \in \text{résultat} : \text{do3} \leq \text{note} \leq \text{do6}\}$

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

Why it 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): classical 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	$\langle e, \sigma \rangle \Longrightarrow \langle e', \sigma' \rangle$	$\llbracket e \rrbracket : D \to 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	Main 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 (a 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, a 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. One writes the invariants, 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)
retirer (montant : INTEGER)
    require
        montant > 0
        solde >= montant
    do
        solde := solde - montant
    ensure
        solde = old solde - montant
        solde >= 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 $\text{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 $\text{wp}$ calculus is, in a way, the “mechanized” version of Hoare logic. For the assignment axiom, $\text{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: one “works 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]$ does.
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: the postcondition has been weakened.
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 correctness proofs for loops.
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: $\text{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 each occurrence of variable $x$ with expression $e$ in 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.
$\wedge$ (conjunction): logical connector “and”. $P \wedge Q$ is true if and only if both $P$ and $Q$ are true.
$\lnot$ (negation): logical connector “not”. $\lnot P$ is true if and only if $P$ is false.
$\Longrightarrow$ (implication): logical connector “implies”. $P \Longrightarrow 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 Series L completed. For application to BP3, see: B1

← Back to index

Proving a Program is Correct

Where Does This Article Fit In?

Why Is This 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 Correctness 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