Proving programs, not just testing them
In 1994 the number theorist Thomas Nicely, computing the sum of the reciprocals of the twin primes, noticed that his new Pentium processor divided some floating-point numbers wrongly. A few entries were missing from a lookup table used by the division circuit; Intel replaced the chips at a cost it put at about 475 million dollars. In 1996 the first Ariane 5 rocket was destroyed about 40 seconds after lift-off because software reused from Ariane 4 converted a 64-bit floating-point number to a 16-bit integer that could not hold it. Both systems had been tested extensively. As Dijkstra put it in 1970, testing can show the presence of bugs, but never their absence.
Formal methods treat programs, circuits and protocols as mathematical objects and prove theorems about them. They have succeeded spectacularly where the stakes justify the effort: the CompCert C compiler (Leroy, from 2006) carries a machine-checked proof that compilation preserves the meaning of programs; the seL4 microkernel (Klein et al., 2009) has a proof that its C code implements its specification; Intel and AMD formally verify their floating-point units; Amazon Web Services checks the designs of its distributed storage systems with the TLA+ model checker, which found errors whose shortest traces had dozens of steps; the driverless Line 14 of the Paris Métro (1998) runs software developed with the B method.
This lesson develops the mathematics underneath: what a program means (operational semantics), how to prove what it does (Hoare logic, with invariants and variants), how to check finite systems exhaustively (model checking, by fixed points), how type systems rule out a class of errors automatically (progress and preservation), and why none of this can ever be fully automated (Rice's theorem).
Three ways to be sure
To prove anything about a program we first need a precise definition of what running it does. That is a semantics: a mathematical relation between programs, initial states and outcomes. Everything else is measured against it.
- Deductive verification proves that every run satisfies a specification, using a logic whose rules follow the program's structure. The creative step is the loop invariant, a statement true before and after every iteration — the program-proving analogue of an induction hypothesis.
- Model checking works with a finite model of the system and checks a temporal property by exploring every reachable state. It is fully automatic, and when the property fails it returns a concrete counterexample run. Its enemy is the size of the state space.
- Type systems assign types to program phrases by simple, compositional rules. A sound type system guarantees, automatically and for every program it accepts, that a certain class of errors never happens.
These approaches trade expressiveness against automation. Rice's theorem says the corner where every property of every program is decided automatically is empty — so each method restricts something: the programs (finite-state), the properties (types), or the automation (a human supplies invariants and proofs).
The lesson uses first-order logic for assertions and soundness arguments, the λ-calculus for reduction and typing, correctness proofs by invariants from algorithm design, and the halting problem from computability.
Semantics, Hoare triples, temporal logic and types
Definition— IMP and its states
A state is a function . Arithmetic expressions and boolean tests denote functions of the state, written and . Commands are
We write for the state that agrees with except that it sends to .
Definition— big-step operational semantics
The relation (" run from terminates in ") is the smallest relation closed under the rules
A judgement holds exactly when it has a finite derivation tree built from these rules. A run that never terminates has no derivation.
The last-but-one rule is not compositional: its premise mentions the same loop. So properties of are proved by induction on derivations (rule induction), not by induction on the command. A small-step semantics describes single computation steps instead; it can also talk about non-terminating and concurrent runs, and the two semantics agree on terminating runs.
Definition— Hoare triple
Let be assertions (predicates on states). The partial-correctness triple is valid, written , if for all states : if and , then . The total-correctness triple additionally requires that from every with the command terminates.
A partial-correctness triple says nothing about runs that do not terminate.
Definition— Hoare logic
The judgement is generated by the rules
where is the assertion : assignment works backwards by substitution. In the loop rule, is the loop invariant.
Definition— weakest precondition
The weakest liberal precondition is the set of states from which every terminating run of ends in ; the weakest precondition also demands termination (Dijkstra). So iff , and , . For loops, is a greatest fixed point, which is why verifiers ask the user for invariants.
Definition— Kripke structure and CTL
A Kripke structure has a set of states , a transition relation in which every state has a successor, and a labelling saying which atomic propositions hold in each state. A path is an infinite sequence . Formulas of computation tree logic (CTL) are
where if some successor satisfies ; if along some path from , eventually holds and holds until then; and if along some path holds forever. The usual abbreviations are ("possibly eventually"), ("always, on every path") and ("inevitably"). Model checking is deciding whether for a given finite , state and formula .
A safety property says something bad never happens (); a liveness property says something good eventually happens ().
Definition— type soundness
Given a small-step reduction and a set of values, a term is stuck if it is not a value and cannot reduce. A type system is sound if no well-typed term ever reduces to a stuck term. The standard proof (Wright and Felleisen, 1994) has two parts: progress (a well-typed term is a value or can reduce) and preservation (reduction preserves types).
Examples
Example— Division by repeated subtraction
The program
should satisfy . Take the invariant . The proof outline is
The program has disappeared from three verification conditions: ; ; and the postcondition. Each is elementary integer arithmetic. Termination needs a separate argument, a variant: the integer is bounded below by by the invariant and decreases by in each iteration.
Example— A too-weak invariant
With the first two verification conditions still hold, but the exit condition fails (take , , , ). This refutes the proof attempt, not the program: invariants must be strong enough to be inductive and to imply the goal. Finding them is where human insight (or a clever algorithm) enters.
Example— Partial correctness without termination
Let . No judgement is derivable, so is valid: a program that never stops satisfies every partial-correctness specification. The loop rule derives it too, with invariant : from we get , and .
Example— A mutual-exclusion protocol as a Kripke structure
Two processes each cycle through idle, trying and critical, and share some flags. A state records both program counters and the flags; transitions interleave single atomic steps. The specification has a safety part, , and liveness parts such as (process can always still get in) and, under a fairness assumption, . The computation below checks three protocols: one violates mutual exclusion, one deadlocks, and Peterson's algorithm (1981) satisfies all three properties it checks.
Example— Typed and stuck terms
In the language of booleans and numbers used below, has type and reduces in two steps to the value . The term is stuck — and ill-typed. The term is well-typed and reduces to : whether that is what the programmer wanted is not a question the type system answers.
The central theorems
Theorem— Theorem 1 (determinism of IMP)
If and then .
Proof
Induction on the derivation of , for all simultaneously. In each case the shape of restricts the last rule of the second derivation . For and assignment both derivations are single axioms with the same conclusion. For , has premises and , and has and ; by the induction hypothesis , and then . For and , both derivations must use the rule for the same value of , since cannot be both and ; the remaining premises are handled exactly as for sequencing (for with , first the body, then the loop from the intermediate state, using the induction hypothesis for the sub-derivation).
∎
Theorem— Theorem 2 (soundness of Hoare logic)
If then .
Proof
Induction on the derivation of . Suppose and .
- Skip. The only rule gives , so .
- Assignment. Then , and the precondition holds at , which by definition means .
- Sequence. The run decomposes as and . The induction hypothesis for the first premise gives , and for the second .
- Conditional. If the run is a run of from a state satisfying ; apply the hypothesis for the first premise. Otherwise use the second.
- Consequence. gives , the hypothesis gives , and gives .
- Loop. By the induction hypothesis, . We show by a second induction, on the derivation of , that implies . If the last rule is the one for , then and we are done. Otherwise , and by a smaller derivation. From we get , and the inner induction hypothesis gives .
∎
The inner induction cannot be replaced by induction on the command: unfolding the loop produces the same loop again. It can be read as induction on the number of iterations — which is finite precisely because we only consider terminating runs.
Theorem— Theorem 3 (total correctness of DIV)
From every state with and , terminates in a state with and .
Proof
The final property is Theorem 2 applied to the proof outline above. For termination, prove by strong induction on : from every state with and the loop terminates. If the loop stops at once. Otherwise one iteration leads to a state with and the same , from which the loop terminates by the induction hypothesis; the loop rule for assembles the two runs. The initialisation sets , so the hypothesis applies with .
∎
The converse of soundness is subtler. Hoare logic for IMP over the integers cannot be complete with a computably enumerable proof system: is valid exactly when halts on no input, and that set of programs is not computably enumerable. What holds is relative completeness:
Theorem— Theorem 4 (relative completeness; Cook 1978) — stated, not proved here
Suppose the assertion language can express the weakest liberal precondition of every command and postcondition (it does for IMP with first-order arithmetic, via Gödel's coding of finite sequences). Then every valid triple is derivable, provided the rule of consequence may use every true assertion as an axiom.
So all the difficulty is pushed into the assertion language. Clarke (1979) showed that for some combinations of language features (for example procedures passed as parameters, together with recursion, static scope and global variables) no sound and relatively complete Hoare logic exists. See Apt, de Boer and Olderog (2009) for proofs.
Theorem— Theorem 5 (EF as a least fixed point)
Let be a transition system and . Define the monotone map on subsets of , where . Then is the least fixed point . If is finite, the iterates , increase and reach after at most steps.
Proof
is monotone, so by the Knaster–Tarski theorem its least fixed point exists and equals the intersection of all with . First, : a state of reaches in zero steps, and a state with a successor in reaches through it. Hence . Conversely let be any fixed point and a path. By backward induction on , , and gives ; so , and .
For the iteration: , and monotonicity gives for all ; also by induction (). A strictly increasing chain of subsets of has at most members, so for some . Then is a fixed point contained in , hence equal to it.
∎
In the same way and , a greatest fixed point. Computing the iterates naively costs per operator, but each least fixed point is really a backward graph search, and is the set of states from which a path inside leads to a non-trivial strongly connected component of the subgraph spanned by the -states. Labelling the subformulas from the inside out therefore gives:
Theorem— Theorem 6 (Clarke, Emerson and Sistla 1986) — proof sketched above
CTL model checking can be done in time .
The catch is that is usually exponential in the size of the system's description: processes with local states each give up to global states (the state-explosion problem). Linear temporal logic (LTL) model checking is linear in but PSPACE-complete in the formula (Sistla and Clarke, 1985).
For type soundness consider the terms with types and , the obvious typing rules, values , and the numerals , and reduction rules such as , for a numeral , and congruence rules that reduce inside , , and (Pierce 2002, chapter 8; all rules are in the Lean code below).
Theorem— Theorem 7 (progress, preservation and safety)
(a) If then is a value or for some . (b) If and then . (c) Hence if and , then is not stuck.
Proof
Canonical forms: a value of type is or , and a value of type is a numeral — by inspecting the typing rules that can type a value.
(a) Induction on the typing derivation. Constants are values. For with : by the induction hypothesis is a value — then or by canonical forms, and one of the two rules applies — or , and the congruence rule applies. The cases , and are the same, using canonical forms for : for instance with a numeral reduces to if and to if .
(b) Induction on the typing derivation, inverting the reduction step. The only non-trivial case is , where we need : numerals have type by an easy induction. Congruence steps follow from the induction hypothesis.
(c) Induction on the number of steps using (b), then (a) at the end.
∎
Theorem— Theorem 8 (Rice 1953)
Let be a set of partial computable functions with and not containing all of them. Then is undecidable, where is the function computed by program .
Proof
Replacing by its complement if necessary, assume the nowhere-defined function is not in , and fix a program with . For a program and input , let be the program that on input first runs on and, if that halts, returns . Then if halts on , and otherwise. The map is computable (the s-m-n theorem). So a decision procedure for would decide the halting problem, which is undecidable (Turing 1936).
∎
Rice's theorem concerns exact decision of semantic properties of all programs. It leaves room for everything formal methods actually do: deciding properties of finite-state models; sound but incomplete automatic analyses that may answer "don't know" (type systems, abstract interpretation); bounded checks; and proofs found with human help.
What a verification result is relative to
A verification theorem has the shape "the artefact satisfies the specification, under these semantics and assumptions". Every part can be wrong in a way the proof cannot detect:
- The specification may not say what was meant. A sorting function specified only to return a sorted list is satisfied by the function that always returns the empty list; the specification must also say the output is a permutation of the input.
- The semantics may not match reality: the formal model of C, of the processor or of the network may differ from the real thing, for instance on undefined behaviour, weak memory or timing.
- The trusted base — the proof checker's kernel, the compiler that built it, the hardware it ran on, and any unverified tools around the verified core — is assumed correct. In 2011 a random-testing study of C compilers (Yang, Chen, Eide and Regehr) found wrong-code bugs in every compiler it tested except in the verified middle part of CompCert; the bugs it found in CompCert were in front-end components that were not verified at the time.
Proof assistants keep the trusted base small: Lean, Coq (now Rocq), Isabelle and HOL Light check every proof with a small kernel, following the design of Milner's LCF system (1972–79) and de Bruijn's earlier criterion that proofs should be checkable by a small, simple program. The proofs on this page are checked by Lean's kernel; you still have to read each statement to know what has been proved.
Compiler correctness is proved by simulation. A relation between source and target states is preserved by computation: whenever and the source takes a step , the target can take one or more steps with .
Pasting squares shows that every source run is matched by a target run. For a deterministic target language this forward simulation also gives the converse direction that one really wants — every behaviour of the compiled code is a behaviour of the source — which is how CompCert's main theorem is proved (Leroy 2009).
Semantics, Hoare logic and model checking in Lean
The Lean module defines IMP with commands as an inductive type and expressions embedded shallowly: an arithmetic expression is any Lean function State → ℤ. This keeps the development short, at the price that the assertion language is all of Lean's logic (so the question of relative completeness does not arise).
/-- Commands of the language IMP. Expressions are shallowly embedded: an arithmetic expression
is a function `State → ℤ` and a test is a function `State → Bool`. -/
inductive Com where
/-- Do nothing. -/
| skip
/-- `x := a`. -/
| assign (x : String) (a : State → ℤ)
/-- `c₁; c₂`. -/
| seq (c₁ c₂ : Com)
/-- `if b then c₁ else c₂`. -/
| ite (b : State → Bool) (c₁ c₂ : Com)
/-- `while b do c`. -/
| while (b : State → Bool) (c : Com)/-- Big-step operational semantics: `BigStep c s t` says that running `c` from state `s`
terminates in state `t`. Each constructor is one inference rule; a derivation is a finite tree,
so a non-terminating run has no derivation at all. -/
inductive BigStep : Com → State → State → Prop where
| skip (s : State) : BigStep .skip s s
| assign (x : String) (a : State → ℤ) (s : State) :
BigStep (.assign x a) s (Function.update s x (a s))
| seq {c₁ c₂ : Com} {s t u : State} :
BigStep c₁ s t → BigStep c₂ t u → BigStep (.seq c₁ c₂) s u
| ite_true {b : State → Bool} {c₁ c₂ : Com} {s t : State} :
b s = true → BigStep c₁ s t → BigStep (.ite b c₁ c₂) s t
| ite_false {b : State → Bool} {c₁ c₂ : Com} {s t : State} :
b s = false → BigStep c₂ s t → BigStep (.ite b c₁ c₂) s t
| while_true {b : State → Bool} {c : Com} {s t u : State} :
b s = true → BigStep c s t → BigStep (.while b c) t u → BigStep (.while b c) s u
| while_false {b : State → Bool} {c : Com} {s : State} :
b s = false → BigStep (.while b c) s sTheorem 1 is an induction on the derivation, exactly as in the proof above:
/-- **Determinism.** If `c` run from `s` can end in `t` and in `t'`, then `t = t'`.
Proof by induction on the derivation of `BigStep c s t`, inverting the second derivation in
each case; in the `if` and `while` cases the test cannot be both true and false. -/
theorem bigStep_deterministic {c : Com} {s t t' : State}
(h : BigStep c s t) (h' : BigStep c s t') : t = t' := by
induction h generalizing t' with
| skip => cases h'; rfl
| assign => cases h'; rfl
| seq _ _ ih₁ ih₂ =>
cases h' with
| seq h₁ h₂ => exact ih₂ (ih₁ h₁ ▸ h₂)
| ite_true hb _ ih =>
cases h' with
| ite_true _ h₂ => exact ih h₂
| ite_false hb' _ => simp_all
| ite_false hb _ ih =>
cases h' with
| ite_true hb' _ => simp_all
| ite_false _ h₂ => exact ih h₂
| while_true hb _ _ ih₁ ih₂ =>
cases h' with
| while_true _ h₁ h₂ => exact ih₂ (ih₁ h₁ ▸ h₂)
| while_false hb' => simp_all
| while_false hb =>
cases h' with
| while_true hb' _ _ => simp_all
| while_false _ => rflValidity of a triple is a definition about runs; derivability is a separate inductive definition with one constructor per rule of Hoare logic. Soundness (Theorem 2) connects them; the loop case is the separate lemma while_sound, proved by induction on the execution:
/-- The **partial-correctness Hoare triple** `{P} c {Q}`: whenever `P` holds before `c` runs
*and the run terminates*, `Q` holds afterwards. Termination is not part of the claim. -/
def Hoare (P : State → Prop) (c : Com) (Q : State → Prop) : Prop :=
∀ s t, P s → BigStep c s t → Q t/-- The proof rules of Hoare logic. `Derivable P c Q` means the triple has a derivation; it says
nothing yet about running programs — connecting the two is the soundness theorem. -/
inductive Derivable : (State → Prop) → Com → (State → Prop) → Prop where
| skip (P : State → Prop) : Derivable P .skip P
| assign (Q : State → Prop) (x : String) (a : State → ℤ) :
Derivable (fun s => Q (Function.update s x (a s))) (.assign x a) Q
| seq {P Q R : State → Prop} {c₁ c₂ : Com} :
Derivable P c₁ Q → Derivable Q c₂ R → Derivable P (.seq c₁ c₂) R
| ite {P Q : State → Prop} {b : State → Bool} {c₁ c₂ : Com} :
Derivable (fun s => P s ∧ b s = true) c₁ Q →
Derivable (fun s => P s ∧ b s = false) c₂ Q → Derivable P (.ite b c₁ c₂) Q
| while {I : State → Prop} {b : State → Bool} {c : Com} :
Derivable (fun s => I s ∧ b s = true) c I →
Derivable I (.while b c) (fun s => I s ∧ b s = false)
| conseq {P P' Q Q' : State → Prop} {c : Com} :
(∀ s, P' s → P s) → Derivable P c Q → (∀ s, Q s → Q' s) → Derivable P' c Q'/-- The `while` rule is sound: if the body preserves the invariant `I` whenever the test is
true, then after the loop (if it terminates) `I` holds and the test is false. The proof is an
induction on the *execution* — not on the command, which does not get smaller when the loop
unfolds. -/
theorem while_sound {I : State → Prop} {b : State → Bool} {c : Com}
(hbody : Hoare (fun s => I s ∧ b s = true) c I) :
Hoare I (.while b c) (fun s => I s ∧ b s = false) := by
intro s t hI hrun
generalize hw : Com.while b c = w at hrun
induction hrun with
| while_true hb hc _ _ ih₂ =>
cases hw
exact ih₂ (hbody _ _ ⟨hI, hb⟩ hc) rfl
| while_false hb =>
cases hw
exact ⟨hI, hb⟩
| _ => cases hw/-- **Soundness of Hoare logic.** Every derivable triple is valid. Induction on the derivation;
each rule is checked against the big-step semantics, with `while_sound` for loops. -/
theorem soundness {P Q : State → Prop} {c : Com} (h : Derivable P c Q) : Hoare P c Q := by
induction h with
| skip P =>
intro s t hP hrun
cases hrun
exact hP
| assign Q x a =>
intro s t hP hrun
cases hrun
exact hP
| seq _ _ ih₁ ih₂ =>
intro s u hP hrun
cases hrun with
| seq h₁ h₂ => exact ih₂ _ _ (ih₁ _ _ hP h₁) h₂
| ite _ _ ih₁ ih₂ =>
intro s t hP hrun
cases hrun with
| ite_true hb h₁ => exact ih₁ _ _ ⟨hP, hb⟩ h₁
| ite_false hb h₂ => exact ih₂ _ _ ⟨hP, hb⟩ h₂
| «while» _ ih => exact while_sound ih
| conseq hpre _ hpost ih =>
intro s t hP hrun
exact hpost _ (ih _ _ (hpre _ hP) hrun)The division program and its invariant, and its correctness proved inside Hoare logic (the verification conditions are the goals left by the rule of consequence) and transported to the semantics by soundness:
/-- The loop `while b ≤ r do (r := r - b; q := q + 1)`. -/
def divLoop : Com :=
.while (fun s => decide (s "b" ≤ s "r"))
(.seq (.assign "r" (fun s => s "r" - s "b")) (.assign "q" (fun s => s "q" + 1)))/-- The program `r := a; q := 0; while b ≤ r do (r := r - b; q := q + 1)`. -/
def divProg : Com :=
.seq (.assign "r" (fun s => s "a")) (.seq (.assign "q" (fun _ => 0)) divLoop)/-- The loop invariant: `a = q·b + r`, `0 ≤ r` and `0 < b`. -/
def divInv (s : State) : Prop :=
s "a" = s "q" * s "b" + s "r" ∧ 0 ≤ s "r" ∧ 0 < s "b"/-- **Partial correctness of division**, proved *inside Hoare logic* and then transported to the
semantics by `soundness`:
`{0 ≤ a ∧ 0 < b} divProg {a = q·b + r ∧ 0 ≤ r < b}`.
The only creative step is the invariant `divInv`; the rest is the verification conditions
`pre → I[q:=0][r:=a]`, `I ∧ b ≤ r → I[q:=q+1][r:=r-b]` and `I ∧ ¬(b ≤ r) → post`. -/
theorem div_correct :
Hoare (fun s => 0 ≤ s "a" ∧ 0 < s "b") divProg
(fun t => t "a" = t "q" * t "b" + t "r" ∧ 0 ≤ t "r" ∧ t "r" < t "b") := by
apply soundness
-- the loop body preserves the invariant
have body : Derivable (fun s => divInv s ∧ decide (s "b" ≤ s "r") = true)
(.seq (.assign "r" (fun s => s "r" - s "b")) (.assign "q" (fun s => s "q" + 1))) divInv := by
refine .conseq ?_ (.seq (.assign _ _ _) (.assign divInv _ _)) (fun _ h => h)
intro s ⟨⟨ha, hr, hb⟩, hle⟩
simp only [decide_eq_true_eq] at hle
simp only [divInv, Function.update_apply]
simp only [String.reduceEq, ite_false, ite_true]
refine ⟨by rw [ha]; ring, by linarith, hb⟩
refine .conseq ?_ (.seq (.assign _ _ _) (.seq (.assign _ _ _) (.while body))) ?_
· intro s ⟨ha, hb⟩
simp only [divInv, Function.update_apply]
simp only [String.reduceEq, ite_false, ite_true]
exact ⟨by ring, ha, hb⟩
· intro t ⟨⟨ha, hr, _⟩, hlt⟩
simp only [decide_eq_false_iff_not, not_le] at hlt
exact ⟨ha, hr, hlt⟩Termination is proved separately from the variant , by strong induction (Theorem 3):
/-- **Termination of the loop.** The *variant* `r` is a natural-number measure that the body
decreases (because `b > 0`) and the loop stops before it goes negative. Formally: strong
induction on `n ≥ r`. -/
theorem divLoop_terminates (n : ℕ) :
∀ s : State, s "r" ≤ n → 0 < s "b" → ∃ t, BigStep divLoop s t := by
induction n using Nat.strong_induction_on with
| _ n ih =>
intro s hr hb
by_cases hle : s "b" ≤ s "r"
· -- one iteration, then the induction hypothesis for the smaller value of `r`
set s₁ := Function.update s "r" (s "r" - s "b") with hs₁
set s₂ := Function.update s₁ "q" (s₁ "q" + 1) with hs₂
have hr₂ : s₂ "r" = s "r" - s "b" := by simp [s₂, s₁]
have hb₂ : s₂ "b" = s "b" := by simp [s₂, s₁]
have hn : 0 < n := by omega
obtain ⟨t, ht⟩ := ih (Int.toNat (s "r" - s "b")) (by omega) s₂ (by omega) (by omega)
exact ⟨t, .while_true (by simpa using hle)
(.seq (.assign _ _ _) (.assign _ _ _)) ht⟩
· exact ⟨s, .while_false (by simpa using hle)⟩/-- **Total correctness, the termination half**: from every state with `0 ≤ a` and `0 < b` the
division program terminates. Together with `div_correct` this is total correctness. -/
theorem div_terminates (s : State) (ha : 0 ≤ s "a") (hb : 0 < s "b") :
∃ t, BigStep divProg s t := by
set s₁ := Function.update s "r" (s "a") with hs₁
set s₂ := Function.update s₁ "q" 0 with hs₂
have hr : s₂ "r" = s "a" := by simp [s₂, s₁]
have hb₂ : s₂ "b" = s "b" := by simp [s₂, s₁]
obtain ⟨t, ht⟩ := divLoop_terminates (Int.toNat (s "a")) s₂ (by omega) (by omega)
exact ⟨t, .seq (.assign _ _ _) (.seq (.assign _ _ _) ht)⟩The diverging loop and the vacuously valid triple :
/-- `while true do skip` has no terminating run from any state: a derivation would have to end
with `while_false`, whose test is false. Induction on the (hypothetical) derivation. -/
theorem loopForever_diverges (s t : State) : ¬ BigStep loopForever s t := by
intro h
generalize hw : loopForever = w at h
induction h with
| while_true _ _ _ _ ih₂ => exact ih₂ hw
| while_false hb =>
cases hw
simp at hb
| _ => cases hw/-- Hence the triple `{true} while true do skip {false}` is **valid** as a partial-correctness
statement — vacuously, because no run terminates. Partial correctness promises nothing about
termination. -/
theorem loopForever_hoare : Hoare (fun _ => True) loopForever (fun _ => False) :=
fun s t _ h => loopForever_diverges s t hType soundness (Theorem 7) for the language of booleans and numbers — typing, reduction, progress, preservation and their combination:
/-- The typing relation `t : T`. -/
inductive HasType : Tm → Ty → Prop where
| tru : HasType .tru .bool
| fls : HasType .fls .bool
| ite {c t e : Tm} {T : Ty} :
HasType c .bool → HasType t T → HasType e T → HasType (.ite c t e) T
| zero : HasType .zero .nat
| succ {t : Tm} : HasType t .nat → HasType (.succ t) .nat
| pred {t : Tm} : HasType t .nat → HasType (.pred t) .nat
| iszero {t : Tm} : HasType t .nat → HasType (.iszero t) .bool/-- Small-step reduction. A term that is not a value and cannot step is **stuck**, such as
`succ tru` or `if zero then … else …`. -/
inductive Step : Tm → Tm → Prop where
| ite_tru {t e : Tm} : Step (.ite .tru t e) t
| ite_fls {t e : Tm} : Step (.ite .fls t e) e
| ite {c c' t e : Tm} : Step c c' → Step (.ite c t e) (.ite c' t e)
| succ {t t' : Tm} : Step t t' → Step (.succ t) (.succ t')
| pred_zero : Step (.pred .zero) .zero
| pred_succ {v : Tm} : NumVal v → Step (.pred (.succ v)) v
| pred {t t' : Tm} : Step t t' → Step (.pred t) (.pred t')
| iszero_zero : Step (.iszero .zero) .tru
| iszero_succ {v : Tm} : NumVal v → Step (.iszero (.succ v)) .fls
| iszero {t t' : Tm} : Step t t' → Step (.iszero t) (.iszero t')/-- **Progress.** A well-typed term is a value or can take a step. Induction on the typing
derivation, using the *canonical forms*: a value of type `bool` is `tru` or `fls`, and a value
of type `nat` is a numeric value. -/
theorem progress {t : Tm} {T : Ty} (h : HasType t T) : Value t ∨ ∃ t', Step t t' := by
induction h with
| tru => exact .inl .tru
| fls => exact .inl .fls
| zero => exact .inl (.num .zero)
| @ite c t e T hc _ _ ihc _ _ =>
right
rcases ihc with hv | ⟨c', hs⟩
· cases hv with
| tru => exact ⟨t, .ite_tru⟩
| fls => exact ⟨e, .ite_fls⟩
| num hn => cases hn <;> cases hc
· exact ⟨_, .ite hs⟩
| succ _ ih =>
rcases ih with hv | ⟨t', hs⟩
· cases hv with
| tru => contradiction
| fls => contradiction
| num hn => exact .inl (.num (.succ hn))
· exact .inr ⟨_, .succ hs⟩
| pred _ ih =>
right
rcases ih with hv | ⟨t', hs⟩
· cases hv with
| tru => contradiction
| fls => contradiction
| num hn =>
cases hn with
| zero => exact ⟨_, .pred_zero⟩
| succ hn => exact ⟨_, .pred_succ hn⟩
· exact ⟨_, .pred hs⟩
| iszero _ ih =>
right
rcases ih with hv | ⟨t', hs⟩
· cases hv with
| tru => contradiction
| fls => contradiction
| num hn =>
cases hn with
| zero => exact ⟨_, .iszero_zero⟩
| succ hn => exact ⟨_, .iszero_succ hn⟩
· exact ⟨_, .iszero hs⟩/-- **Preservation.** Reduction preserves types: if `t : T` and `t ⟶ t'` then `t' : T`.
Induction on the typing derivation, inverting the step. -/
theorem preservation {t t' : Tm} {T : Ty} (h : HasType t T) (hs : Step t t') :
HasType t' T := by
induction h generalizing t' with
| tru => cases hs
| fls => cases hs
| zero => cases hs
| ite hc ht he ihc _ _ =>
cases hs with
| ite_tru => exact ht
| ite_fls => exact he
| ite hs' => exact .ite (ihc hs') ht he
| succ _ ih =>
cases hs with
| succ hs' => exact .succ (ih hs')
| pred ht ih =>
cases hs with
| pred_zero => exact .zero
| pred_succ hv => exact numVal_hasType hv
| pred hs' => exact .pred (ih hs')
| iszero _ ih =>
cases hs with
| iszero_zero => exact .tru
| iszero_succ _ => exact .fls
| iszero hs' => exact .iszero (ih hs')/-- **Type safety** ("well-typed programs cannot go wrong", Milner): every term reachable from a
well-typed term by any number of steps is a value or can step again — it is never stuck.
Induction on the reduction sequence, using preservation at each step and progress at the end. -/
theorem type_safety {t t' : Tm} {T : Ty} (h : HasType t T)
(hs : Relation.ReflTransGen Step t t') : Value t' ∨ ∃ t'', Step t' t'' := by
have : HasType t' T := by
induction hs with
| refl => exact h
| tail _ hstep ih => exact preservation ih hstep
exact progress thisTheorem 5 for an arbitrary (possibly infinite) transition system, using Mathlib's Knaster–Tarski least fixed point OrderHom.lfp:
/-- In a transition system with relation `R`, the CTL formula `EF φ` ("along some path, φ
eventually holds") is satisfied by the states from which a `φ`-state is reachable. -/
def EF {S : Type*} (R : S → S → Prop) (φ : Set S) : Set S :=
{s | ∃ t, Relation.ReflTransGen R s t ∧ t ∈ φ}/-- The monotone operator `Z ↦ φ ∪ pre(Z)`, where `pre(Z)` is the set of states with a
successor in `Z`. A model checker computes `EF φ` by iterating it from `∅`. -/
def efStep {S : Type*} (R : S → S → Prop) (φ : Set S) : Set S →o Set S where
toFun Z := φ ∪ {s | ∃ t, R s t ∧ t ∈ Z}
monotone' := fun _ _ hZ _ hs =>
hs.elim Or.inl fun ⟨t, hst, ht⟩ => Or.inr ⟨t, hst, hZ ht⟩/-- **`EF φ = μZ. φ ∪ pre(Z)`.** The set `EF φ` is the least fixed point of `efStep` (which
exists by the Knaster–Tarski theorem, Mathlib's `OrderHom.lfp`). One inclusion: `EF φ` is closed
under the operator, so it contains the least fixed point (`OrderHom.lfp_le`). The other: by
induction along a path to `φ`, every state of `EF φ` lies in every fixed point. -/
theorem ef_eq_lfp {S : Type*} (R : S → S → Prop) (φ : Set S) :
EF R φ = OrderHom.lfp (efStep R φ) := by
apply le_antisymm
· rintro s ⟨t, hst, ht⟩
have hfix := OrderHom.map_lfp (efStep R φ)
induction hst using Relation.ReflTransGen.head_induction_on with
| refl => rw [← hfix]; exact Or.inl ht
| head hsu _ ih => rw [← hfix]; exact Or.inr ⟨_, hsu, ih⟩
· apply OrderHom.lfp_le
rintro s (hs | ⟨u, hsu, t, hut, ht⟩)
· exact ⟨s, .refl, hs⟩
· exact ⟨t, .head hsu hut, ht⟩Finally, Rice's theorem (Theorem 8), applied from Mathlib's computability library, where programs are codes for partial recursive functions:
/-- **Rice's theorem.** Let `C` be a set of partial functions `ℕ →. ℕ` such that membership of
a program's *behaviour* in `C` is decidable. If one partial recursive function lies in `C`, all
of them do: every decidable semantic property is trivial. This applies Mathlib's
`ComputablePred.rice`. -/
theorem rice (C : Set (ℕ →. ℕ))
(h : ComputablePred fun c => Nat.Partrec.Code.eval c ∈ C)
{f g : ℕ →. ℕ} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f ∈ C) : g ∈ C :=
ComputablePred.rice C h hf hg fCWhat is formalised: Theorems 1, 2, 3, 5 (the fixed-point characterisation, without the iteration bound) and 7 are proved here; Theorem 8 is Mathlib's. Not formalised: relative completeness (Theorem 4), the other CTL operators and the complexity bound (Theorem 6), small-step semantics for IMP, and any connection to real programs or hardware.
Model checking and verification conditions, by computer
The first experiment is a small explicit-state model checker. It explores every interleaving of two processes for three mutual-exclusion protocols by breadth-first search, returns a shortest counterexample when mutual exclusion fails, finds the deadlock of the second protocol, and computes by the fixed-point iteration of Theorem 5 — the printed sizes are the iterates .
"""Explicit-state model checking of three mutual-exclusion protocols.
Two processes share boolean flags (and, for Peterson's algorithm, a variable
``turn``). Every interleaving of their atomic steps is explored by
breadth-first search, so each reported property is checked on the *whole*
finite state space of the model: this is exhaustive, exact evidence about the
model. Breadth-first search also returns a *shortest* counterexample when a
property fails. The CTL property AG EF crit0 ("from every reachable state,
process 0 can still reach its critical section") is computed as a least fixed
point, Z_{k+1} = crit0 U pre(Z_k), exactly as in the lesson's Lean theorem
``ef_eq_lfp``. What is verified is the model, not real code on real hardware.
"""
from collections import deque
# A state is (pc0, pc1, flag0, flag1, turn).
INITIAL = (0, 0, False, False, 0)
def _with(state, i, pc=None, flag=None, turn=None):
"""Return a copy of ``state`` with process i's pc/flag (and turn) changed."""
pcs, flags = [state[0], state[1]], [state[2], state[3]]
if pc is not None:
pcs[i] = pc
if flag is not None:
flags[i] = flag
return (pcs[0], pcs[1], flags[0], flags[1],
state[4] if turn is None else turn)
def step_check_then_set(state, i):
"""Naive protocol: look at the other flag, then raise our own."""
j, pc = 1 - i, state[i]
if pc == 0:
return _with(state, i, pc=1)
if pc == 1: # enter only if the other flag is down
return None if state[2 + j] else _with(state, i, pc=2)
if pc == 2:
return _with(state, i, pc=3, flag=True)
return _with(state, i, pc=0, flag=False) # pc 3 = critical: leave
def step_set_then_check(state, i):
"""Raise our flag first, then wait until the other flag is down."""
j, pc = 1 - i, state[i]
if pc == 0:
return _with(state, i, pc=1)
if pc == 1:
return _with(state, i, pc=2, flag=True)
if pc == 2:
return None if state[2 + j] else _with(state, i, pc=3)
return _with(state, i, pc=0, flag=False) # pc 3 = critical: leave
def step_peterson(state, i):
"""Peterson's algorithm: flag[i] := true; turn := j; await; critical."""
j, pc = 1 - i, state[i]
if pc == 0:
return _with(state, i, pc=1)
if pc == 1:
return _with(state, i, pc=2, flag=True)
if pc == 2:
return _with(state, i, pc=3, turn=j)
if pc == 3:
go = (not state[2 + j]) or state[4] == i
return _with(state, i, pc=4) if go else None
return _with(state, i, pc=0, flag=False) # pc 4 = critical: leave
#: name -> (step function, critical pc)
PROTOCOLS = {
"check-then-set": (step_check_then_set, 3),
"set-then-check": (step_set_then_check, 3),
"Peterson": (step_peterson, 4),
}
def successors(step, state):
"""All states reachable in one atomic step of either process."""
return [t for t in (step(state, 0), step(state, 1)) if t is not None]
def explore(step):
"""Breadth-first search; return (parent map, successor map)."""
parent, succ = {INITIAL: None}, {}
queue = deque([INITIAL])
while queue:
s = queue.popleft()
succ[s] = successors(step, s)
for t in succ[s]:
if t not in parent:
parent[t] = s
queue.append(t)
return parent, succ
def trace_to(parent, state):
"""The BFS path from the initial state to ``state`` (a shortest path)."""
path = []
while state is not None:
path.append(state)
state = parent[state]
return path[::-1]
def ef_fixpoint(succ, goal):
"""Least fixed point of Z -> goal U pre(Z); return (set, sizes of iterates)."""
z, sizes = set(), []
while True:
new = {s for s in succ if s in goal or any(t in z for t in succ[s])}
sizes.append(len(new))
if new == z:
return z, sizes
z = new
def check(name):
"""Model-check one protocol; return a dict of results."""
step, crit = PROTOCOLS[name]
parent, succ = explore(step)
bad = [s for s in parent if s[0] == crit and s[1] == crit]
dead = [s for s in parent if not succ[s]]
goal = {s for s in succ if s[0] == crit}
ef, sizes = ef_fixpoint(succ, goal)
return {
"states": len(parent),
"mutex": not bad,
"counterexample": trace_to(parent, min(bad, key=lambda s: len(
trace_to(parent, s)))) if bad else None,
"deadlocks": dead,
"ag_ef_crit0": set(succ) <= ef,
"ef_sizes": sizes,
}
def describe(state):
"""Short text for a state."""
flags = "".join("T" if f else "F" for f in state[2:4])
return f"pc=({state[0]},{state[1]}) flags={flags} turn={state[4]}"
def main():
print("Explicit-state model checking, two processes, all interleavings")
print(f"{'protocol':<16}{'states':>7} {'mutual excl.':<14}"
f"{'deadlock-free':<15}AG EF crit0")
results = {name: check(name) for name in PROTOCOLS}
for name, r in results.items():
mutex = "holds" if r["mutex"] else "VIOLATED"
dead = "yes" if not r["deadlocks"] else "NO"
ag = "yes" if r["ag_ef_crit0"] else "no"
print(f"{name:<16}{r['states']:>7} {mutex:<14}{dead:<15}{ag}")
print()
print("Shortest counterexample to mutual exclusion (check-then-set):")
for k, s in enumerate(results["check-then-set"]["counterexample"]):
print(f" {k}: {describe(s)}")
print("Both processes are now at pc 3, the critical section.")
print()
print("Deadlocked states of set-then-check (no process can move):")
for s in results["set-then-check"]["deadlocks"]:
print(f" {describe(s)}")
sizes = results["Peterson"]["ef_sizes"]
print("Peterson: sizes of the iterates of Z -> crit0 U pre(Z) from the empty")
print("set: " + ", ".join(map(str, sizes)) + " (stable = the least fixed point)")
print()
print("Epistemic status: exhaustive and exact for these finite models - every")
print("reachable state was examined, and the counterexample and deadlock are")
print("concrete runs. It says nothing about real code, compilers or weak")
print("memory hardware, and starvation freedom needs fairness assumptions")
print("that are not modelled; Peterson's correctness in general is a theorem.")
if __name__ == "__main__":
main()This is exhaustive evidence about each finite model. The model is interleaving semantics with atomic reads and writes; on real multiprocessors with weak memory, Peterson's algorithm needs memory fences.
The second experiment mechanises the proof outline of the division program: a weakest-precondition calculus (assignment is substitution) produces the verification conditions, SymPy checks their equational parts exactly, and every integer point of a small box is tested. With the weak invariant the box search finds the counterexample to the exit condition shown in the examples.
"""From Hoare logic to algebra: verification conditions for integer division.
The program r := a; q := 0; while b <= r do (r := r - b; q := q + 1) is
annotated with a loop invariant. A weakest-precondition calculus (assignment
is substitution, wp(c1; c2, Q) = wp(c1, wp(c2, Q))) turns the annotated program
into three verification conditions (VCs): plain implications between integer
formulas, with no program left in them. SymPy performs the substitutions
symbolically. Each VC is then checked twice: its equational part by symbolic
algebra (exact), and the whole implication on every integer point of a box
(exhaustive for the box only - not a proof for all integers). A deliberately
weak invariant produces a VC with a counterexample, and random testing of the
program itself is shown for contrast.
"""
import itertools
import random
import sympy
a, b, q, r = sympy.symbols("a b q r", integer=True)
VARS = (a, b, q, r)
PRE = sympy.And(a >= 0, b > 0)
POST = sympy.And(sympy.Eq(a, q * b + r), r >= 0, r < b)
GOOD_INV = sympy.And(sympy.Eq(a, q * b + r), r >= 0, b > 0)
WEAK_INV = sympy.And(sympy.Eq(a, q * b + r), b > 0) # forgets r >= 0
GUARD = b <= r
BODY = [(r, r - b), (q, q + 1)] # r := r-b; q := q+1
INIT = [(r, a), (q, sympy.Integer(0))] # r := a; q := 0
def wp_assignments(assignments, post):
"""Weakest precondition of a sequence of assignments: substitute backwards."""
for var, expr in reversed(assignments):
post = post.subs(var, expr, simultaneous=True)
return post
def verification_conditions(inv):
"""The three VCs (name, hypothesis, conclusion) for the annotated program."""
return [
("entry", PRE, wp_assignments(INIT, inv)),
("preservation", sympy.And(inv, GUARD), wp_assignments(BODY, inv)),
("exit", sympy.And(inv, sympy.Not(GUARD)), POST),
]
def equations_reduce(hyp, concl):
"""Do the equations in ``concl`` follow from a = q*b + r by algebra alone?"""
eqs = [c for c in sympy.And.make_args(concl) if isinstance(c, sympy.Eq)]
return all(sympy.expand((e.lhs - e.rhs).subs(a, q * b + r)) == 0
for e in eqs)
def box_counterexample(hyp, concl, radius):
"""First integer point in [-radius, radius]^4 where hyp holds and concl fails."""
holds_hyp = sympy.lambdify(VARS, hyp, modules="math")
holds_concl = sympy.lambdify(VARS, concl, modules="math")
rng = range(-radius, radius + 1)
for point in itertools.product(rng, repeat=4):
if holds_hyp(*point) and not holds_concl(*point):
return point
return None
def fmt(formula):
"""Compact text for a conjunction of (in)equalities, e.g. 'a = b*q + r, r >= 0'."""
parts = []
for c in sympy.And.make_args(formula):
op = "=" if isinstance(c, sympy.Eq) else c.rel_op
parts.append(f"{sympy.sstr(c.lhs)} {op} {sympy.sstr(c.rhs)}")
return ", ".join(parts)
def run_program(a0, b0):
"""Execute the program directly; return (q, r)."""
r0, q0 = a0, 0
while b0 <= r0:
r0, q0 = r0 - b0, q0 + 1
return q0, r0
def random_tests(n, seed=2024):
"""Run the program on n random inputs with a >= 0, b > 0; count failures."""
rng = random.Random(seed)
failures = 0
for _ in range(n):
a0, b0 = rng.randint(0, 10**4), rng.randint(1, 100)
q0, r0 = run_program(a0, b0)
failures += not (a0 == q0 * b0 + r0 and 0 <= r0 < b0)
return failures
def main():
radius = 4
print("Program: r := a; q := 0; while b <= r do (r := r - b; q := q + 1)")
print("Pre: a >= 0, b > 0. Post: a = q*b + r, r >= 0, r < b.")
for label, inv in [("I", GOOD_INV), ("weak I (no r >= 0)", WEAK_INV)]:
print()
print(f"{label}: {fmt(inv)}")
names = {"entry": "Pre ==> wp(r := a; q := 0, I):",
"preservation": "I, b <= r ==> wp(body, I):",
"exit": "I, b > r ==> Post:"}
for name, hyp, concl in verification_conditions(inv):
alg = "yes" if equations_reduce(hyp, concl) else "no"
cex = box_counterexample(hyp, concl, radius)
box = "none" if cex is None else "(a, b, q, r) = " + str(cex)
print(f" VC {name}: {names[name]}")
print(f" {fmt(concl)}")
print(f" algebra: {alg}; counterexample in box: {box}")
print()
print(f"Box = all {(2 * radius + 1) ** 4} integer points of "
f"[-{radius}, {radius}]^4.")
print(f"Random tests of the program itself: 2000 runs, "
f"{random_tests(2000)} failures.")
print()
print("Epistemic status: the substitutions and the algebraic reductions are")
print("exact symbolic computations; the box search is exhaustive only on the")
print("box and the random tests cover 2000 inputs, so neither proves the VCs")
print("for all integers (the inequalities follow by linear arithmetic, as in")
print("the Lean proof div_correct). The weak invariant's failed VC refutes")
print("that proof attempt, not the program, which is correct.")
if __name__ == "__main__":
main()Industrial verifiers such as Dafny and Why3 work this way, discharging the verification conditions with SMT solvers — decision procedures for combinations of theories like linear integer arithmetic — rather than with a box search.
Explore: an inductive invariant is a tautology
Hardware model checkers reduce safety to propositional logic. A 2-bit counter with state steps ; its next state is given by and . To show the state is never reached, check that the invariant holds initially (it does: the counter starts at ) and is inductive: invariant now and one transition imply invariant next. The table below shows that this implication is a tautology.
Is the invariant ¬(a ∧ b) inductive?
Type a formula of propositional logic and see its value in every possible case.
Read as: ((¬(a ∧ b) ∧ (c ↔ b)) ∧ (d ↔ (¬a ∧ ¬b))) → ¬(c ∧ d)
Use the symbols ¬ ∧ ∨ → ↔, the words not, and, or, implies, iff, or ASCII ~ & | -> <->. Variables are single lowercase letters. ¬ binds tightest, then ∧, ∨, →, ↔; p → q → r means p → (q → r).
Tautology — true in all 16 rows.
| a | b | c | d | (¬(a ∧ b) ∧ (c ↔ b)) ∧ (d ↔ ¬a ∧ ¬b) → ¬(c ∧ d) |
|---|---|---|---|---|
| T | T | T | T | T |
| T | T | T | F | T |
| T | T | F | T | T |
| T | T | F | F | T |
| T | F | T | T | T |
| T | F | T | F | T |
| T | F | F | T | T |
| T | F | F | F | T |
| F | T | T | T | T |
| F | T | T | F | T |
| F | T | F | T | T |
| F | T | F | F | T |
| F | F | T | T | T |
| F | F | T | F | T |
| F | F | F | T | T |
| F | F | F | F | T |
16 rows: one for every way of making the 4 variables true or false.
Now introduce a bug: in the box, replace (not a and not b) by not a. The formula is no longer a tautology. Find the falsifying row: it is , , , , a transition from into — and the buggy counter really does reach from , so this is a genuine bug, not just a failure of induction. (In general a falsifying row may start from an unreachable state; then the invariant must be strengthened.) SAT solvers decide such questions for millions of variables, and techniques such as -induction and IC3 construct inductive invariants automatically.
Exercises
1. Formal methods
Warm-upHumanWhich of these are valid partial-correctness triples over the integers? (Choose all that apply.)
2. Formal methods
Warm-upHumanCompute . It has the form . What is ?
3. Formal methods
CoreHumanThe program should satisfy . Which loop invariant lets the loop rule and the rule of consequence prove this?
4. Formal methods
CoreHumanIn the soundness proof of Hoare logic, the loop case is proved by induction on the derivation of . Why would structural induction on the command not work?
5. Formal methods
CoreHumanWhich CTL formula says: from every reachable state it is possible to get back to an initial state (a "reset" property)?
6. Formal methods
CoreComputationalA Kripke structure has states and transitions , , , , , . The proposition holds only in state . Compute by the iteration , . How many states satisfy ?
7. Formal methods
CoreHumanPrograms are written in a Turing-complete language. Which of these problems are undecidable? (Choose all that apply.)
8. Formal methods
CoreFormalWhich Lean definition correctly formalises the partial-correctness triple , where BigStep c s t means that c run from s terminates in t?
9. Formal methods
CoreHumanA compiler comes with a machine-checked proof that, whenever it succeeds, the generated assembly has only behaviours allowed by the source program, according to formal semantics of the source and assembly languages. Which of the following could still lead to a wrongly behaving executable? (Choose all that apply.)
10. Formal methods
StretchComputationalWrite find_violation(initial, successors, is_bad) for explicit-state model checking of a safety property. successors(s) returns a list of states and is_bad(s) a boolean. Return a shortest path [initial, ..., bad_state] to a reachable bad state, or None if no reachable state is bad. Your search must terminate on finite systems with cycles.
Common misconceptions
Misconception
"A verified program is correct." It is correct relative to its specification, the semantics used in the proof, and its trusted base. A wrong specification, an unfaithful model of the hardware or an unverified component can still let errors through — as the discussion of CompCert's front end shows.
Misconception
"Partial correctness implies termination." is valid. Termination is a separate obligation, discharged by a variant: a quantity in a well-founded order that every iteration decreases.
Misconception
"Model checking proves the program correct." It decides whether a finite model satisfies a property. The model may abstract away the very feature that causes the bug, or be cut off at a bound; and a property such as says nothing about properties that were not checked, such as liveness.
Misconception
"Rice's theorem makes verification impossible." It rules out a single algorithm that decides every semantic property for every program. Verification of specific programs, analyses that may answer "don't know", finite-state model checking and interactive proof are all untouched.
Misconception
"A well-typed program has no bugs." Type soundness excludes stuck states — such as applying to a boolean — and nothing else. Logical errors, wrong results and non-termination are all compatible with a sound type system (unless the types are rich enough to express the specification, as in Lean).
Many ways of seeing
Topology— Safety is closed, liveness is dense
Give the set of infinite runs over a finite set of states the product topology, with metric (a Cantor space). A property is a safety property — every violation is witnessed by a finite bad prefix — exactly when is closed; it is a liveness property — every finite prefix can be extended into — exactly when is dense. Every property is the intersection of the two: , and the second set is dense (Alpern and Schneider, 1985). Topology explains why safety is checked by looking for finite counterexamples, while liveness needs cycles in the state graph. See point-set topology.
Geometry— The geometry of concurrency
Dijkstra (1968) drew two processes as a rectangle: one axis records the progress of each process, an execution is a path increasing in both coordinates, and a resource that only one process may hold at a time removes a forbidden rectangle. If the processes take two locks in opposite orders, two forbidden rectangles form a cross (the "Swiss flag"), and there is a region below it from which every increasing path gets stuck: a deadlock, visible as a corner of the geometry. Fajstrup, Goubault and Raussen (1998) turned this into an algorithm, and directed algebraic topology studies such spaces of increasing paths up to directed homotopy: deforming an execution through executions does not change its result, so the essentially different schedules are counted by a topological invariant rather than enumerated one interleaving at a time.
Algebra— Programs as elements of an algebra
In a Kleene algebra with tests (Kozen, 1997) programs are elements of an idempotent semiring with a star operation, tests form a Boolean subalgebra, and , . A Hoare triple becomes the equation , and Hoare's rules become theorems of the algebra; the equational theory of KAT is decidable (PSPACE-complete). Predicate transformers give another algebraic picture: strongest postcondition and weakest liberal precondition form a Galois connection, . See algebraic structures and order theory.
Computation— Where the cost goes
CTL model checking is linear in the model and the formula (Theorem 6); LTL is PSPACE-complete in the formula. The real difficulty is that the model is exponentially large. Symbolic model checking represents sets of states by binary decision diagrams (Bryant, 1986; Burch, Clarke, McMillan and others, 1990) and computes the fixed points of Theorem 5 on those representations; bounded model checking (Biere, Cimatti, Clarke and Zhu, 1999) asks a SAT solver for a counterexample of length at most ; partial-order reduction avoids exploring interleavings that commute. On the deductive side, SMT solvers decide the verification conditions that tools like Dafny and Why3 generate. See computational complexity.
Logic— Why completeness can only be relative
Hoare logic sits on top of an assertion logic, and inherits its incompleteness: by Gödel, the true first-order sentences of arithmetic are not computably enumerable, and the valid triples encode the complement of the halting problem. Cook's theorem isolates exactly this: the program-logic rules are complete, and all incompleteness lives in the assertion language. In a dependently typed proof assistant such as Lean the distinction blurs — specifications are types, and by the Curry–Howard correspondence a verified program is a term together with a proof (see type theory and the incompleteness theorems).
History and global context
- First proofs of programs. Goldstine and von Neumann (1947) annotated flow diagrams with assertion boxes. Turing's three-page paper Checking a large routine (1949) proved a factorial routine correct with assertions and a termination argument by a decreasing quantity.
- Program logics. Floyd's Assigning meanings to programs (1967) attached assertions to flowcharts; Hoare's An axiomatic basis for computer programming (1969) turned them into a logic; Dijkstra's guarded commands and weakest preconditions (1975, A Discipline of Programming, 1976) made the calculus a method for deriving programs. Cook (1978) proved relative completeness and Clarke (1979) its limits.
- Semantics. Scott and Strachey founded denotational semantics around 1970, with Scott's domain theory giving meaning to recursion as a least fixed point. Plotkin's Aarhus lecture notes (1981) introduced structural operational semantics; Kahn's natural semantics (1987) is the big-step style used here.
- Temporal logic and model checking. Pnueli proposed temporal logic for programs in 1977. Model checking was invented independently by Clarke and Emerson (1981) in the United States and by Queille and Sifakis (1982) in France; Clarke, Emerson and Sifakis received the 2007 Turing Award.
- Types. Milner's slogan "well-typed programs cannot go wrong" (1978) and Wright and Felleisen's syntactic method (1994) gave the progress-and-preservation proofs used today. Milner's LCF system (1972–79) introduced the small trusted kernel used by modern proof assistants; de Bruijn's Automath (from 1967) was the first system for checking mathematics by computer.
- Methods and industry. VDM grew out of IBM's Vienna laboratory in the 1970s; Abrial's Z notation and B method came from Oxford and France, B being used for the Paris Métro Line 14. Patrick and Radhia Cousot introduced abstract interpretation in 1977; their Astrée analyser has been used on Airbus flight-control software. Zhou Chaochen, with Hoare and Ravn, created the Duration Calculus for real-time systems (1991), and He Jifeng and Hoare developed the Unifying Theories of Programming (1998). The United Nations University's International Institute for Software Technology, which opened in Macau in 1992, trained researchers from many developing countries in formal methods.
Further reading
- Glynn Winskel, The Formal Semantics of Programming Languages (1993) — operational and denotational semantics, Hoare logic and completeness.
- Tobias Nipkow and Gerwin Klein, Concrete Semantics with Isabelle/HOL (2014) — IMP, Hoare logic and type systems, all machine-checked.
- Michael Huth and Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems (2nd ed., 2004) — CTL, LTL, model checking and program verification.
- Christel Baier and Joost-Pieter Katoen, Principles of Model Checking (2008) — the standard graduate text.
- Benjamin C. Pierce, Types and Programming Languages (2002) — chapter 8 is the type-soundness proof above.
- Krzysztof R. Apt, Frank S. de Boer and Ernst-Rüdiger Olderog, Verification of Sequential and Concurrent Programs (3rd ed., 2009) — soundness and relative completeness in full.
- C. A. R. Hoare, "An axiomatic basis for computer programming", Communications of the ACM (1969); Xavier Leroy, "Formal verification of a realistic compiler", Communications of the ACM (2009).