Axiomatic Semantics and Hoare Logic
Denotational semantics told us what a program is — a function on states. Axiomatic semantics
asks a sharper, more practical question: what can we prove about it? Instead of computing a
program's meaning, we reason about the assertions that hold before and after it runs.
The vehicle is the Hoare triple, introduced by Tony Hoare in 1969 in a paper whose
title — "An Axiomatic Basis for Computer Programming" — announced the ambition to make programming a
deductive science.
\{P\}\; c\; \{Q\}
Read it aloud: "if the precondition P holds of the state, and we run
c, then if c halts the postcondition
Q holds of the resulting state." Here P and
Q are logical formulae about the program variables — predicates over the same
state space \Sigma we met in the
denotational semantics of IMP.
(An undergraduate treatment is the
Hoare-logic
page; here we press on to the full proof system and its meaning.)
Partial versus total correctness
That innocent phrase "if c halts" hides a fork in the road. The triple above
is a claim of partial correctness: it promises the right answer provided the
program terminates, and says nothing at all when it loops forever. Termination is a separate,
harder promise.
-
Partial correctness \{P\}\, c\, \{Q\}: for every state
satisfying P, if executing c
terminates, the final state satisfies Q. A non-terminating
c makes the triple vacuously true.
-
Total correctness [P]\, c\, [Q]: for every state
satisfying P, execution of c
does terminate and the final state satisfies Q.
Slogan: total = partial + termination. The loop
\mathtt{while}\ \mathtt{true}\ \mathtt{do}\ \mathtt{skip} satisfies
every partial triple \{P\}\, c\, \{Q\} — it never terminates, so
there is never a bad final state to catch it out — yet it satisfies no total triple at all. All but the
final rule below concern partial correctness; termination we handle with a variant on the next
page.
The proof rules
Hoare logic is a formal proof system: each syntactic construct of IMP gets one
inference rule, read "if the triples above the line are derivable, so is the one below". The genius is
that the rules are syntax-directed — the shape of the command tells you which rule to apply —
so a proof mirrors the program's structure.
\dfrac{}{\ \{\,Q[a/x]\,\}\; x := a\; \{\,Q\,\}\ }
To make Q hold after x := a, require
that Q with a textually substituted for
x holds before. It runs "backwards", and that is exactly why it is
the cornerstone of weakest-precondition reasoning.
The rule surprises everyone the first time. To end with
\{\,x = 5\,\} after x := y + 1, substitute
y+1 for x in the postcondition to get the
precondition \{\,y + 1 = 5\,\}, i.e. \{\,y = 4\,\}.
Substitution flows from post to pre.
\dfrac{\ \{P\}\; c_1\; \{R\} \qquad \{R\}\; c_2\; \{Q\}\ }{\ \{P\}\; c_1;\, c_2\; \{Q\}\ }
Thread the two triples through a shared middle assertion R: whatever holds
after c_1 is the precondition for c_2.
\dfrac{\ \{P \wedge b\}\; c_1\; \{Q\} \qquad \{P \wedge \neg b\}\; c_2\; \{Q\}\ }{\ \{P\}\; \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2\; \{Q\}\ }
Each branch may assume the guard's truth value; both must re-establish the same
Q.
\dfrac{\ P \Rightarrow P' \qquad \{P'\}\; c\; \{Q'\} \qquad Q' \Rightarrow Q\ }{\ \{P\}\; c\; \{Q\}\ }
The bridge between logic and program: you may always strengthen a precondition or
weaken a postcondition, discharging the implications in ordinary logic.
The while rule and the loop invariant
Everything so far was mechanical; the loop is where correctness proofs demand insight. The
while rule rests on a single, hand-supplied idea: an invariant
I, an assertion that is true before the loop and preserved by every
iteration.
\dfrac{\ \{\,I \wedge b\,\}\; c\; \{\,I\,\}\ }{\ \{\,I\,\}\; \mathtt{while}\ b\ \mathtt{do}\ c\; \{\,I \wedge \neg b\,\}\ }
If the body c preserves I whenever the guard
b is true, then after the whole loop I still holds
— and the loop only exits when b is false, so we learn
I \wedge \neg b.
The invariant is the loop's essence distilled into one formula. It must satisfy three duties, and a
proof is really the act of finding a formula that meets all three at once:
\underbrace{P \Rightarrow I}_{\text{established on entry}} \qquad \underbrace{\{I \wedge b\}\; c\; \{I\}}_{\text{preserved by the body}} \qquad \underbrace{(I \wedge \neg b) \Rightarrow Q}_{\text{delivers the goal on exit}}
Choosing I is a genuinely creative step — too weak and it does not imply
Q; too strong and the body breaks it. Below is the Hasse-diagram intuition:
assertions ordered by logical implication form a lattice, and the invariant must sit in a
"just-right" band between P and Q.
In this lattice, P \Rightarrow Q means P sits
below Q (a stronger assertion is lower — it rules out more states).
\mathsf{false} is the bottom (implies everything), and
\mathsf{true} is the top (implied by everything). The rule of consequence is
exactly permission to slide down at the precondition and up at the postcondition.
A full worked proof
Let us prove that this program computes the sum
0 + 1 + \cdots + (n-1) into s, for
n \ge 0:
{ n >= 0 }
s := 0 ;
i := 0 ;
while (i < n) do
s := s + i ;
i := i + 1
{ s = n*(n-1)/2 }
The creative step is the invariant. We claim
I \;\equiv\; \Big(\, 0 \le i \le n \ \wedge\ s = \tfrac{i(i-1)}{2} \,\Big):
"so far we have added up the first i numbers". Now discharge the three
duties.
-
Establishment. After s:=0;\ i:=0 we have
i = 0, s = 0. With n \ge 0 this gives
0 \le 0 \le n and s = \tfrac{0\cdot(-1)}{2} = 0
— so I holds. ✓
-
Preservation. Assume I \wedge i < n. The body sets
s' = s + i = \tfrac{i(i-1)}{2} + i = \tfrac{i(i+1)}{2} and
i' = i + 1. Then
s' = \tfrac{i'(i'-1)}{2} and, since
i < n, 0 \le i' \le n. So
I holds again. ✓
-
Exit. On exit I \wedge \neg(i < n) gives
i \le n and i \ge n, hence
i = n, so s = \tfrac{n(n-1)}{2} — exactly
Q. ✓
Three checks, and the program is proved partially correct. The proof did not run the loop even once —
it reasoned about all executions at a stroke, which is the whole point.
Checking a triple against the semantics
A Hoare triple is a syntactic object; its meaning is a claim about the denotational
function of the command. We can sample that claim: pick many states satisfying
P, run c, and check
Q holds after. This does not prove a triple (only a derivation
does), but it is a superb way to refute a wrong one and to gain confidence in a candidate
invariant.
type State = Record<string, number>;
// Interpreter for the sum program: s := 0; i := 0; while (i= 0 } prog { Q } over many states satisfying the precondition P: n >= 0.
let ok = true;
for (let n = 0; n <= 12; n++) {
const out = runSum({ n, s: 0, i: 0 });
const good = post(out);
if (!good) { ok = false; console.log(`FAIL n=${n}: s=${out.s}, expected ${(n * (n - 1)) / 2}`); }
}
console.log("Triple { n>=0 } sum { s = n(n-1)/2 } held on all tested states? " + ok);
// Spot-check the invariant is preserved by one body step from a valid mid-loop state.
const mid: State = { n: 6, i: 3, s: 3 }; // s = 3 = 3*2/2 ✓
console.log("invariant at mid state? " + invariant(mid));
const stepped = { ...mid, s: mid.s + mid.i, i: mid.i + 1 };
console.log("invariant after one body step? " + invariant(stepped));
Every sampled state confirms the triple, and the invariant survives a body step — the empirical shadow
of the paper proof above. Testing complements verification; it never replaces it.
Tony Hoare has a famous confession and a famous triumph, and they sit oddly together. The confession:
in 1965, designing ALGOL W, he introduced the null reference "simply because it was so
easy to implement" — a decision he later called his "billion-dollar mistake", for the endless
crashes and vulnerabilities that null-pointer dereferences have caused across every language that copied
it. The triumph, just four years later: the 1969 paper that founded the logic on this page, giving us a
way to prove programs free of exactly such errors. There is a lovely irony that the same person
gave the world both its most expensive footgun and one of its sharpest tools for reasoning code into
correctness. Hoare also invented Quicksort (aged 26, in Moscow) — the man has range.
Two traps peculiar to Hoare logic. First, partial correctness is vacuous for diverging
programs: \{\mathsf{true}\}\ \mathtt{while}\ \mathtt{true}\ \mathtt{do}\ \mathtt{skip}\ \{\mathsf{false}\}
is derivable and true, because the loop never reaches a final state to violate
\mathsf{false}. If you actually care that the program produces an answer,
you need total correctness and a termination argument — the partial-correctness while rule will
happily "prove" nonsense about a loop that spins forever. Second, an invariant that is too
weak (say, just 0 \le i \le n without the
s = \tfrac{i(i-1)}{2} conjunct) is perfectly preserved by the body
yet fails the exit obligation — it does not imply Q. Preservation
alone is not enough; the invariant must be strong enough to deliver the goal and weak enough to
survive the body. Finding that balance is the whole art.