Programs and correctness
This chapter verifies two small imperative programs: an assignment sequence and a while loop. We build a fragment of dynamic logic, which expresses how programs affect states, then derive rules of Hoare logic for reasoning about preconditions and postconditions.
Registering the Floyd assignment axiom with @rewrite lets the compiler
compute assignment preconditions by substitution. The examples prove
partial correctness: if a program terminates, its result satisfies the
postcondition. They do not prove termination.
Formulas and programs
Two sorts represent data: obj for program-variable values and world for
program states. The object syntax has only 0 and pred; this example
needs no arithmetic laws. Formulas are a separate syntactic sort form,
since the provable sort wff is reserved for judgments about them.
Programs use four constructs. Sequencing a ⨟ b runs a then b.
Iteration ⋆ a runs a zero or more times. A test ? p leaves the state
unchanged if p holds and cannot proceed otherwise. Assignment ⟨ x ≔ e ⟩
stores the value of e in x.
The formula [ a ] p says that p holds after every terminating run of
a.
Judgments
The basic judgment is world-labelled truth: w : p says the formula p
holds at state w, and step w a v says program a can move state w to
state v. Sequents g ⊢ w : p collect labelled assumptions in a context
that behaves as a set, as in Natural deduction. ⊨ p asserts truth at every state. The Hoare triple ⦃ p ⦄ a ⟦ q ⟧ says that
every terminating run of a from a state satisfying p ends in a state
satisfying q.
Equivalence infrastructure
Each sort gets its equivalence, bundled for the normalizer as in Equality and normalization.
Congruence rules let rewriting pass through the surrounding constructors used in these proofs.
Substitution as computation
The substitution operators get the standard @rewrite annotations, as in the
Peano and lambda calculus chapters:
The logic
The propositional core is a labelled natural deduction system. These are the rules of the Natural deduction chapter, with world indices.
pbc makes the base logic classical.
The modality needs only two rules. K and necessitation are derivable:
To prove [ a ] p at w, box_intro assumes that a reaches an arbitrary
state v and proves p is true in that state. The bound binder {v: world}
makes v an eigenvariable: the rule’s dependency lists keep it out of the
other arguments, so the proof cannot depend on a particular choice of
destination state.
Reduction axioms
Compound programs reduce to their parts. Sequencing and test are genuine rewrites; the box over a compound program is the simpler formula:
red_assign is the Floyd assignment axiom: the box over an assignment is the
substitution instance. Because it is a @rewrite, and the substitution
operators push through the formula language by rewrites too, checking any line
against a boxed assignment computes the weakest precondition.
Iteration is different: star_fix is not a rewrite. Its right-hand side
mentions [ ⋆ a ] again, so normalizing with it would loop. Unfolding a loop
is a deliberate proof step. star_ind is the corresponding induction rule.
Validity and Hoare triples
valid_intro proves validity by proving the formula at an arbitrary state
from an empty context. The two ht rules convert between a Hoare triple ⦃ p ⦄ a ⟦ q ⟧ and ⊨ (p → ([ a ] q)). The while loop is a definition, not a
primitive: iterate the guarded body, then exit through the failed guard.
The modal toolkit
A few validity-level lemmas are useful. box_k is the K axiom.
The reduction axioms rewrite left to right, so proofs that need to build a
box (introducing [ a ⨟ b ] p from its reduct) cite these symmetric forms
through at_mp.
Note the pool worlds: imp_refl_valid has no world binder of its own, so
u and v come from the sort’s @vars pool and become the eigenstates that
valid_intro and box_intro discharge.
Hoare logic, derived
We can now derive Hoare rules for consequence, sequencing, assignment, and while loops.
Assignment comes in two forms. The Floyd–Hoare assignment rule follows from
red_assign:
The @view described in Views and recovery lets
proof lines omit the explicit substitution ⌊ x / e ⌋ p. Its phantom binder
q occupies the precondition, while the assignment and postcondition
determine x, e, and p. The rewrite rules then compute the substitution
⌊ x / e ⌋ p.
hoare_assign_wp builds in precondition strengthening. Read its
hypothesis as “q implies the weakest precondition”. Its view again lets us
lean on the rewrite rules to handle substitutions. The phantom r stands where
⌊ x / e ⌋ p sits in the raw rule, so the cited verification condition can be
written with the substitutions fully evaluated.
The last line states the triple with while b a; the compiler matches it
against l20’s unfolded form through the definition.
Verified programs
The first program assigns a to x, then overwrites it with b. The first
assignment has no effect on the final result. Its verification condition
reduces to the reflexive equality b = b:
The final program repeatedly assigns pred x to x while x ≠ 0. Its loop
invariant is ⊤, which holds in every state. hoare_while proves that, on
exit, the invariant holds and the guard is false: ⊤ ∧ ¬ ¬ (x = 0).
hoare_conseq then uses classical double-negation elimination to obtain x = 0.
This does not show that the loop reaches zero. We have given pred no
arithmetic axioms, and the proof establishes only the state on termination.