Part 3: A Denotational Semantics for IMP

In Part 1 we set up the basic vocabulary of domain theory, and in Part 2 we saw how Part α realizes the flat domain on α and gives us a fixed-point operator Part.fix together with an induction principle for reasoning about fixpoints. Now we see how we can apply it to basic program verification.

Introduction
The language
Denotational semantics
Hoare logic
Soundness
Worked example: integer division
Total correctness
Conclusion
References

1. Introduction

We’re going to build a toy imperative language with denotational semantics, and show how to verify programs using Hoare logic. We will be using the ideas from the previous to sections meaning to give meaning to programs that may not terminate. With Part.fix at our disposal, the meaning of a while loop is just a least fixed point, and we can prove things about while loops using Scott induction. We will finish with an integer division algorithm written in our toy language, and give a full proof of both termination and correctness using Part theory.

2. The language

We will begin with the syntax. The language is the standard textbook IMP, with arithmetic expressions, boolean expressions, and commands.

inductive aexp where
  | num  : ℕ → aexp
  | var  : String → aexp
  | nAdd : aexp → aexp → aexp
  | nSub : aexp → aexp → aexp
  | nMul : aexp → aexp → aexp

inductive bexp where
  | bTrue  : bexp
  | bFalse : bexp
  | bAnd   : bexp → bexp → bexp
  | bOr    : bexp → bexp → bexp
  | beq    : aexp → aexp → bexp
  | bLe    : aexp → aexp → bexp
  | bGt    : aexp → aexp → bexp
  | bnot   : bexp → bexp

inductive Cmd where
  | cskip  : Cmd
  | cseq   : Cmd → Cmd → Cmd
  | asgn   : String → aexp → Cmd
  | cif    : bexp → Cmd → Cmd → Cmd
  | cwhile : bexp → Cmd → Cmd

Program state is represented by total functions from variable names to natural numbers, with a pointwise update.

abbrev State := String → ℕ

def State.update (s : State) (x : String) (n : ℕ) : State :=
  fun y => if y = x then n else s y

Writing programs as raw Cmd constructors is both ugly and tedious, so I added a quotation macro ⟪ ... ⟫ that lets us write programs in a nicely legible syntax, as well as a bunch of other notational conveniences. I won’t show them here since it’s not interesting but I will be using them moving forward.

example : Cmd := ⟪
  result := 1 ;;
  while x > 0 do
    result := result * x ;;
    x := x - 1
  end
⟫

3. Denotational semantics

We’ve described a grammar for our programs and now we need to state what programs actually compute. The plan is to map each piece of the syntax into a real Lean function. Expressions evaluate to values; commands transform states. Partiality shows up in the semantics of while.

Arithmetic and boolean expressions are straightforward.

def adenote : aexp → State → ℕ
  | .num n,      _ => n
  | .var x,      s => s x
  | .nAdd a₁ a₂, s => adenote a₁ s + adenote a₂ s
  | .nSub a₁ a₂, s => adenote a₁ s - adenote a₂ s
  | .nMul a₁ a₂, s => adenote a₁ s * adenote a₂ s

def bdenote : bexp → State → Bool
  | .bTrue,      _ => true
  | .bFalse,     _ => false
  | .bAnd b₁ b₂, s => bdenote b₁ s && bdenote b₂ s
  | .bOr b₁ b₂,  s => bdenote b₁ s || bdenote b₂ s
  | .beq a₁ a₂,  s => adenote a₁ s == adenote a₂ s
  | .bLe a₁ a₂,  s => Nat.ble (adenote a₁ s) (adenote a₂ s)
  | .bGt a₁ a₂,  s => Nat.blt (adenote a₂ s) (adenote a₁ s)
  | .bnot b,     s => !bdenote b s

Commands are where partiality enters. A command denotes a partial function State →. State (ie. State → Part State). Every case is straightforward except while.

def denote : Cmd → State →. State
  | .cskip,       s => some s
  | .cseq c₁ c₂,  s => do 
    let x ← denote c₁ s
    denote c₂ x
  | .asgn x a,    s => some (s.update x (adenote a s))
  | .cif b c₁ c₂, s => if bdenote b s then denote c₁ s else denote c₂ s
  | .cwhile b c,  s =>
      Part.fix (fun (rec : State →. State) (s : State) =>
        if bdenote b s then do
          let x ← denote c s
          rec x
        else some s) s

Looking at the while case, we’re saying that denote (while b do c) is the least fixed point of the functional

\[F(\mathrm{rec})(s) = \begin{cases} \mathrm{rec}(\llbracket c \rrbracket(s)) & \text{if } \llbracket b \rrbracket(s) \\ s & \text{otherwise.} \end{cases}\]

Remember from part 1, this is the recursive equation a while loop satisfies, written as a fixed-point equation. Part.fix applies to any functional, so writing the denotation down doesn’t require a precondition. Continuity is what guarantees Part.fix F actually satisfies $F(\mathrm{Part.fix}\,F) = \mathrm{Part.fix}\,F$, which is what makes this the meaning of a while loop and not just some arbitrary partial function.

Our F is ω-Scott continuous since it’s built from continuous pieces, and (State →. State) is a domain, so we have a meaningful least fixed point.

4. Hoare logic

We have a programming language, and now we need a way to reason about programs in our language, that is, we need a program logic. The canonical choice for sequential imperative programs is Hoare logic. Hoare logic consists of assertions about the program state and a set of inference rules for reasoning about program state.

Judgments are triples ${P}\, c\, {Q}$ read as “if $P$ holds before running $c$, and $c$ terminates, then $Q$ holds afterward”. The rules are as follows.

\[\frac{}{\{P\}\ \texttt{skip}\ \{P\}}\;\textsc{(skip)} \qquad \frac{}{\{P[a/x]\}\ x := a\ \{P\}}\;\textsc{(assign)}\] \[\frac{\{P\}\ c_1\ \{Q\} \quad \{Q\}\ c_2\ \{R\}}{\{P\}\ c_1;\,c_2\ \{R\}}\;\textsc{(seq)}\] \[\frac{\{P \land b\}\ c_1\ \{Q\} \quad \{P \land \neg b\}\ c_2\ \{Q\}}{\{P\}\ \texttt{if } b \texttt{ then } c_1 \texttt{ else } c_2\ \{Q\}}\;\textsc{(if)}\] \[\frac{\{P \land b\}\ c\ \{P\}}{\{P\}\ \texttt{while } b \texttt{ do } c\ \{P \land \neg b\}}\;\textsc{(while)}\] \[\frac{P \Rightarrow P' \quad \{P'\}\ c\ \{Q'\} \quad Q' \Rightarrow Q}{\{P\}\ c\ \{Q\}}\;\textsc{(conseq)}\]

The (while) rule is the loop-invariant rule. To prove ${P}\,\texttt{while } b \texttt{ do } c\,{P \land \neg b}$, find a $P$ that the body preserves whenever the guard holds. Then on exit, $P$ still holds and the guard is false.

Now to encode this in Lean. First, an assertion is a predicate on states.

abbrev Assertion := State → Prop

Substitution P⟦a / x⟧ is the assertion that P holds after we replace x with the value of a.

def Assertion.subst (P : Assertion) (x : String) (a : aexp) : Assertion :=
  fun s => P (s.update x (adenote a s))

notation:max P "⟦" a:max " / " x:max "⟧" => Assertion.subst P x a

A Hoare triple ⦃P⦄ c ⦃Q⦄ is partial correctness. Starting from a state satisfying P, every state we can reach via denote c satisfies Q. Diverging executions don’t witness anything, so the triple is vacuously satisfied on them.

def HoareTriple (P Q : Assertion) (c : Cmd) :=
  ∀ s₁ s₂, P s₁ → s₂ ∈ (denote c s₁) → Q s₂

notation:max "⦃" P "⦄" c:max "⦃" Q "⦄" => HoareTriple P Q c

The Hoare derivations themselves are an inductive relation, one constructor per rule. This is exactly the inference system at the top of this section.

inductive Hoare : Assertion → Cmd → Assertion → Prop where
  | hoare_skip   : ∀ P,     Hoare P ⟪ skip ⟫ P
  | hoare_assign : ∀ P x a, Hoare (P⟦a / x⟧) ⟪ ‹x› := ‹a› ⟫ P
  | hoare_seq : ∀ P Q R c₁ c₂,
      Hoare P c₁ Q →
      Hoare Q c₂ R →
      Hoare P ⟪ c₁ ;; c₂ ⟫ R
  | hoare_if : ∀ P Q b c₁ c₂,
      Hoare (P.bexp_true b)  c₁ Q →
      Hoare (P.bexp_false b) c₂ Q →
      Hoare P ⟪ if b then c₁ else c₂ end ⟫ Q
  | hoare_while : ∀ P b c,
      Hoare (P.bexp_true b) c P →
      Hoare P ⟪ while b do c end ⟫ (P.bexp_false b)
  | hoare_conseq : ∀ P P' Q Q' c,
      (∀ s, P s → P' s) →
      Hoare P' c Q' →
      (∀ s, Q' s → Q s) →
      Hoare P c Q

5. Soundness

We’ve now got two ways of talking about programs: the denotational semantics from §3 and the Hoare logic from §4. Soundness is what connects them. It says that the syntactic Hoare derivations actually mean what they should under the denotational semantics.

Theorem. Hoare P c Q → ⦃P⦄ c ⦃Q⦄.

The proof is by induction on the Hoare derivation. Most cases are mechanical unfolding. simp together with the definitions of denote and HoareTriple discharges skip, assignment, sequencing, conditionals, and consequence. The interesting case is while. There we have a fixed point and we want to show every state reachable from denote (while b do c) s₁ satisfies P ∧ ¬b.

This is what fix_induction_mem_of_continuous from Part 2 was built for, namely Scott induction specialized to membership claims, with the bottom and chain-closure cases discharged for free.

To use it we have to prove the loop functional is ω-Scott continuous. This is mechanical. Each branch of the body is either a constant (Part.some s) or a bind of a continuous denotation followed by rec. ωScottContinuous.bind and ωScottContinuous.const from Mathlib’s API close both.

| hoare_while P b c h ih =>
  simp only [HoareTriple, denote]
  intro s₁ s₂ Ps₁ hfix
  have hF : ωScottContinuous
      (fun (rec : State → Part State) (s : State) =>
        if bdenote b s then do let x ← denote c s; rec x else Part.some s) := by
    apply ωScottContinuous.of_apply₂
    intro s
    by_cases hb : bdenote b s = Bool.true
    · simp only [hb, if_true]
      exact ωScottContinuous.bind ωScottContinuous.const ωScottContinuous.id
    · simp only [hb, Bool.false_eq_true, if_false]
      exact ωScottContinuous.const
  apply @Part.fix_induction_mem_of_continuous _ _ _
    (fun x y => P x → P.bexp_false b y) hF _ _ _ hfix Ps₁
  intro f ih_f x y hy hPx
  split_ifs at hy <;> rename_i hb
  · simp [Part.mem_bind_iff] at hy
    obtain ⟨z, hz, hyf⟩ := hy
    exact ih_f z y hyf (ih x z ⟨hPx, hb⟩ hz)
  · simp at hy
    subst hy
    exact ⟨hPx, hb⟩

The apply reduces the goal to the step case of Scott induction. We split on the loop guard. When the guard is true we ran the body to some intermediate state z, and the inductive hypothesis says any further iteration from z lands in P ∧ ¬b. When the guard is false we exited with the current state, which already satisfies P ∧ ¬b since we entered with P and b is now false.

This is the loop-invariant preservation argument you’d write informally on a chalkboard, dropped into the step case of Scott induction with the other two cases handled for us.

6. Worked example: integer division

Since soundness is proven, building a Hoare derivation suffices to prove specific IMP programs correct. Integer division by repeated subtraction is the example we will use.

def div_prog : Cmd := ⟪
  q := 0 ;;
  r := m ;;
  while n ≤ r do
    r := r - n ;;
    q := q + 1
  end
⟫

The precondition requires n > 0 and the postcondition gives the standard division spec.

def div_pre : Assertion :=
  fun s => s "n" > 0

def div_post : Assertion :=
  fun s => s "m" = s "q" * s "n" + s "r" ∧ s "r" < s "n"

The loop invariant is the relationship between dividend, divisor, quotient, and remainder, plus the constraint that the divisor is positive (which is needed for the body to behave sensibly).

def div_inv : Assertion :=
  fun s => s "m" = s "q" * s "n" + s "r" ∧ s "n" > 0

The derivation follows the control flow of the program. The body is two assignments in sequence, the while rule wraps it, the initialization sits in front, and consequence patches up the pre and post. The little bit of arithmetic comes in when checking the body preserves the invariant. After simp we have r = (q+1) * n + (r - n) under n ≤ r, which omega closes.

theorem div_correct : ⦃ div_pre ⦄ div_prog ⦃ div_post ⦄ := by
  apply hoare_sound
  -- ... build the derivation as described above

7. Total correctness

Partial correctness is vacuous on diverging programs, which is why the soundness theorem doesn’t carry a termination obligation. To prove a program correct we want to show partial correctness and termination. Terminates says the denotation is defined on every state satisfying the precondition.

def Terminates (P : Assertion) (c : Cmd) : Prop :=
  ∀ s, P s → (denote c s).Dom

def HoareTotal (P Q : Assertion) (c : Cmd) : Prop :=
  ⦃P⦄ c ⦃Q⦄ ∧ Terminates P c

notation:max "⦃" P "⦄ₜ " c:max " ⦃" Q "⦄" => HoareTotal P Q c

For division, termination reduces to showing Part.fix divLoopF is defined on every input satisfying the precondition. Since divLoopF is ω-Scott continuous, Part.fix divLoopF = divLoopF (Part.fix divLoopF), so we can unfold the fix one step at a time and recurse on a well-founded measure. The variant for the division loop is r, which strictly decreases by at least n ≥ 1 per iteration.

We factor out the loop body as a stand alone def and prove it continuous using Mathlib’s API.

def divStep (t : State) : State :=
  (t.update "r" (t "r" - t "n")).update "q" (t "q" + 1)

def divLoopF : (State → Part State) → State → Part State :=
  fun rec t =>
    if bdenote ⟪b| n ≤ r⟫ t then rec (divStep t) else Part.some t

private theorem divLoopF_continuous : ωScottContinuous divLoopF := by
  apply ωScottContinuous.of_apply₂
  intro t
  by_cases hb : bdenote ⟪b| n ≤ r⟫ t = Bool.true
  · simp only [divLoopF, hb, if_true]
    exact ωScottContinuous.apply (divStep t)
  · simp only [divLoopF, hb, Bool.false_eq_true, if_false]
    exact ωScottContinuous.const

The termination lemma is induction on k with hypothesis t "r" ≤ k. At each step Part.fix_eq_of_ωScottContinuous rewrites Part.fix divLoopF t as divLoopF (Part.fix divLoopF) t, and we case on the loop guard. False branch returns Part.some t, done. True branch recurses on divStep t, whose r is strictly smaller.

private theorem div_loop_dom :
    ∀ (k : ℕ) (t : State), t "r" ≤ k → t "n" > 0 → (Part.fix divLoopF t).Dom := by
  intro k
  induction k with
  | zero =>
    intro t hr hn
    rw [Part.fix_eq_of_ωScottContinuous divLoopF_continuous]
    have hguard : ¬ (bdenote ⟪b| n ≤ r⟫ t = Bool.true) := by
      simp [bdenote, adenote]; omega
    simp [divLoopF, hguard]
  | succ k ih =>
    intro t hr hn
    rw [Part.fix_eq_of_ωScottContinuous divLoopF_continuous]
    by_cases hguard : bdenote ⟪b| n ≤ r⟫ t = Bool.true
    · simp only [divLoopF, hguard, if_true]
      have hle : t "n" ≤ t "r" := by simp [bdenote, adenote] at hguard; omega
      have ht'r : (divStep t) "r" ≤ k := by simp [divStep, State.update]; omega
      have ht'n : (divStep t) "n" > 0 := by simp [divStep, State.update]; exact hn
      exact ih (divStep t) ht'r ht'n
    · simp [divLoopF, hguard]

Then div_terminates is mostly definition pushing. Identify the denotation of div_prog with Part.fix divLoopF applied to the post-init state, then invoke div_loop_dom. Total correctness follows from combining div_correct and div_terminates.

theorem div_terminates : Terminates div_pre div_prog := by
  intro s hn_pre
  let s' : State := (s.update "q" 0).update "r" (s "m")
  have hs'n : s' "n" > 0 := by simp [s', State.update]; exact hn_pre
  have prog_eq : denote div_prog s = Part.fix divLoopF s' := by
    unfold divLoopF
    simp [div_prog, denote, State.update, adenote, s', divStep]
    rfl
  rw [prog_eq]
  exact div_loop_dom (s' "r") s' (le_refl _) hs'n

theorem div_total : ⦃ div_pre ⦄ₜ div_prog ⦃ div_post ⦄ :=
  ⟨div_correct, div_terminates⟩

8. References

Software Foundations, Pierce et al. Volume 2 (Programming Language Foundations)

Table of Contents