Formal Methods: Specifying Before You Build

PredicatePredicate Logic closes by attaching a predicate to a specific point in a program — "when execution reaches here, this must be true." A formal method is what results from taking that idea seriously as an engineering discipline: write a system's requirements as statements in set theory and predicate logic, precise enough that "is this specification self-consistent" and "does this design satisfy that specification" become questions with checkable answers, rather than questions a prose requirements document can only gesture at. It is not a replacement for testing — it catches a different class of error, ambiguity and contradiction in the specification itself, before a single line of implementation exists to test.

The Logical Foundation: Axiomatic Semantics

Hoare'sHoare's axiomatic semantics is the bridge from predicate logic to programs specifically¹. A Hoare triple {P} C {Q} states: if predicate P holds before command C runs, and C terminates, predicate Q holds afterward. P is the precondition, Q the postcondition, and both are ordinary predicate logic formulas of exactly the kind the companion page covers — {balance ≥ withdrawal} withdraw(withdrawal) {balance ≥ 0} says nothing about how withdraw is implemented, only what must be true going in and what's guaranteed coming out. A loop needs one more idea, an invariant — a predicate that's true before the loop starts, stays true after every iteration, and (combined with the loop's exit condition) implies the postcondition once the loop finishes — which is precisely how a loop's correctness gets reduced to a claim about predicate logic rather than a claim about "running it enough times and seeing what happens."

The Z Notation

IndividualIndividual pre/postconditions scale to a whole function; they don't by themselves scale to a whole system's state. Z (pronounced "zed") adds one structuring device on top of set theory and predicate logic to make that jump: the schema, a named box with a signature (the state it declares) above the line and a predicate (the invariant constraining that state) below it². Reusing the library domain from Relational Modelling, a Z schema for the same loans data looks like this:

┌ LibraryLoans ──────────────────────────────
│ books      : ℙ TITLE
│ borrowedBy : TITLE ⇸ MEMBER
├─────────────────────────────────────────────
│ dom borrowedBy ⊆ books
└─────────────────────────────────────────────

┌ BorrowBook ────────────────────────────────
│ ΔLibraryLoans
│ title?  : TITLE
│ member? : MEMBER
├─────────────────────────────────────────────
│ title? ∈ books
│ title? ∉ dom borrowedBy
│ borrowedBy' = borrowedBy ∪ {title? ↦ member?}
└─────────────────────────────────────────────

LibraryLoans declares the state: books is a set (ℙ, "power set of") of titles, and borrowedBy is a partial function (⇸ — not every book is currently borrowed) from titles to members; the predicate below the line is the schema's own invariant, exactly the same "must always be true" idea a class invariant expresses in object-oriented design, stated once instead of re-checked at the top of every method. BorrowBook is an operation schema: ΔLibraryLoans means it changes the state described by LibraryLoans; title? and member? (the ? suffix marks an input) are what the caller supplies; the predicates below the line are the operation's precondition (the book exists and isn't already out) and its effect, with borrowedBy' — the primed name — meaning the state after the operation runs. Reading the schema is, at every point, reading a predicate logic formula over sets; nothing new is introduced beyond notation for keeping a large specification's many small, related formulas organised.

Does It Work? The CICS Case Study

Z'sZ's best-known industrial result is IBM's use of it to specify parts of CICS, a transaction-processing system with thousands of live installations. Oxford University and IBM Hursley jointly used Z on the project through the 1980s, and IBM's own measurements afterward showed a real reduction in defects found post-release, earlier detection of the defects that were found, and roughly a 9% reduction in total development cost for the release involved — significant enough that the work contributed to a Queen's Award for Technological Achievement³. That's a rare thing for a formal method: a large, commercial, non-academic codebase with before-and-after numbers attached, rather than a demonstration on a toy problem.

Myths and Limits

TwoTwo claims about formal methods are common and both wrong in the same direction — overclaiming what the mathematics actually delivers. The first is that a formally verified system is guaranteed bug-free: what's actually guaranteed is that the implementation matches the specification — if the specification itself doesn't capture what users actually needed, a perfectly verified system faithfully implements the wrong thing. Nothing about writing that specification in Z makes it immune to the ordinary failure modes of requirements work — Where Requirements Get Hard covers Meyer's silence and wishful thinking, and the assumptions-engineering discipline for catching them, in full; a Z schema states its invariant with total precision, but precision about the wrong invariant is still the wrong invariant, precisely and unambiguously specified. The second is that formal methods only make sense for exotic, safety-critical software (avionics, nuclear control systems) and are otherwise too expensive to justify — the CICS case above is ordinary commercial transaction-processing software, and the cost reduction came specifically from catching design errors earlier, when they're cheap to fix, rather than after release, when they aren't⁴. Z's actual, narrower limit is scale of a different kind: writing and checking schemas by hand doesn't scale past a certain specification size without tool support (a type-checker for the schema calculus, at minimum), which is exactly why Z is usually reached for on the highest-value, highest-consequence parts of a system's design rather than applied uniformly across an entire codebase.

A schema and a concrete example specification (a BDD scenario, say) are answering different questions about the same system, which raises a question of its own: what would it take to keep the two checked against each other, rather than trusting by hand that a scenario and a schema covering the same operation actually agree? Schemas and Scenarios is a speculative sketch of exactly that, grounded in real research on the general problem rather than treated as an open question nobody has looked at.

References