In the ideal, a software engineer builds software the way an engineer builds a bridge: from a specification whose properties can be ANALYSED before construction. Testing samples the input space; proof covers it entirely. THE MOTIVATION, stated as a comparison: TESTING demonstrates the presence of defects on the inputs you tried. Coverage is a sample. INSPECTION human reading; catches much, but humans reason poorly about concurrency and about very large case-splits. PROOF establishes a property for ALL inputs. If the specification and the proof are right, that class of defect cannot exist. A FORMAL SPECIFICATION is one written in a language with a MATHEMATICALLY DEFINED SYNTAX AND SEMANTICS, so that: · it is UNAMBIGUOUS — there is exactly one reading, which is the property natural language cannot provide (recall the requirements topic) · it can be ANALYSED MECHANICALLY — inconsistencies and incompletenesses can be detected by tool · properties can be PROVEN to follow from it · it can be REFINED to code with the refinement itself proven correct WHERE THE PAYOFF IS LARGEST: writing a formal specification forces the questions nobody asked. Industrial experience reports repeatedly find that most of the value comes not from the proof but from the ACT OF SPECIFYING — the ambiguities surfaced while formalising are defects removed at requirements cost. TWO STYLES OF FORMAL SPECIFICATION: ALGEBRAIC APPROACH — the system is described in terms of OPERATIONS and their RELATIONSHIPS, given as axioms. Suited to specifying interfaces and abstract data types. Example, a stack: pop(push(s, x)) = s top(push(s, x)) = x isEmpty(new()) = true isEmpty(push(s, x)) = false pop(new()) = ERROR Note: no state is described, only the RELATIONS between operations. Languages: Larch, OBJ, Lotos. MODEL-BASED APPROACH — the system is modelled using mathematical constructs such as SETS, SEQUENCES, RELATIONS and FUNCTIONS, and operations are defined by how they change the state. Languages: Z, VDM, B, Alloy. Example, an air-traffic sector as a set: Sector : ℙ Aircraft capacity : ℕ INVARIANT #Sector ≤ capacity Enter(a) ≙ pre a ∉ Sector ∧ #Sector < capacity post Sector' = Sector ∪ {a} Leave(a) ≙ pre a ∈ Sector post Sector' = Sector \ {a} The INVARIANT is the point: it must hold before and after every operation, and proving that it does is what rules out a whole class of failure.

SPECIFY the licence status transition from earlier topics, model-based. STATE Status ::= RECEIVED | UNDER_REVIEW | APPROVED | REJECTED | ISSUED applications : Appl ⇸ Status (a partial function) audit : seq (Appl × Status × Status × Officer) INVARIANTS I1 dom applications ≠ ∅ ⇒ every application has exactly one status (implied by "function") I2 ∀ a ∈ dom applications · applications(a) = ISSUED ⇒ ∃ entry ∈ audit · entry names a and ends ISSUED (no licence is issued without an audit record) OPERATION SetStatus(a : Appl, s : Status, o : Officer) PRE a ∈ dom applications ∧ (applications(a), s) ∈ legalTransitions ∧ authorised(o, s) POST applications' = applications ⊕ {a ↦ s} ∧ audit' = audit ⌢ ⟨(a, applications(a), s, o)⟩ ∧ ∀ b ∈ dom applications · b ≠ a ⇒ applications'(b) = applications(b) WHAT THE FORMALISM FORCED — and this is the real content: 1. THE FRAME CONDITION. That last conjunct says NO OTHER APPLICATION CHANGES. In prose nobody writes this, and yet "the operation modified something it shouldn't have" is a real and common defect class. Formal specification makes the frame problem explicit and impossible to forget. 2. legalTransitions HAD TO BE DEFINED. You cannot write the precondition without enumerating which transitions are legal — exactly the state machine the interface specification topic discovered by asking about error 409. Formality forces the same discovery. 3. THE AUDIT INVARIANT I2 is a property that spans two data structures. Testing can check it on the cases you try; proving it holds after every operation establishes it for all executions. 4. WHAT HAPPENS WHEN THE PRECONDITION FAILS is now a visible, separate question. Prose specifications routinely leave this silent — which is the "incompleteness for invalid input" defect from the SRS topic. PROVING AN INVARIANT PRESERVED — the shape of the argument: assume I2 holds and the precondition holds show I2 holds of applications' and audit' Case s = ISSUED: the postcondition appends an audit entry naming a and ending ISSUED, so the witness required by I2 exists. ✓ Case s ≠ ISSUED: a's new status is not ISSUED, and no other application changed (frame condition), so any application that was ISSUED still has its witness in audit, and audit only grows. ✓ Therefore I2 is preserved by SetStatus. ∎ Note that the second case DEPENDS ON THE FRAME CONDITION. Drop it, and the proof fails — the specification could allow another application's status to change to ISSUED without an audit entry. THE PROOF FOUND THE NEED FOR THE FRAME CONDITION, which is precisely the kind of gap that reaches production otherwise. CLEANROOM SOFTWARE ENGINEERING — the process built around this idea (Mills, IBM): · emphasis on DEFECT AVOIDANCE rather than defect removal · incremental development under statistical quality control · specification is functional and formal (box structure specification: black box → state box → clear box) · CORRECTNESS VERIFICATION replaces unit testing — developers prove their code against its specification and are NOT PERMITTED to test it themselves · independent STATISTICAL USAGE TESTING (see the next topic) certifies reliability Reported results were strong on defect density, but adoption has been limited because it requires mathematical training and a large cultural change.

THE HONEST COSTS: · REQUIRES SPECIALISED TRAINING. Few engineers, and almost no customers, can read Z or B — so a formal specification CANNOT SERVE as the agreed document with the customer. You end up maintaining two specifications. · EXPENSIVE. Specification and proof effort is substantial, and proof effort grows quickly with system size. · POORLY SUITED to specifying user interfaces and user interaction, which is a large part of many systems. · TOOL SUPPORT is far behind mainstream development tooling. · IT PROVES THE CODE MATCHES THE SPECIFICATION — not that the specification is what the customer wanted. Formal methods address VERIFICATION, and validation remains a human problem. A proven-correct implementation of the wrong requirement is still worthless. · THE ENVIRONMENT IS NOT PROVEN. The compiler, the OS, the hardware and the libraries are outside the proof. seL4 addresses this for a microkernel by proving down to the binary, which shows both that it is possible and how much work it is. WHERE FORMAL METHODS PAY FOR THEMSELVES — the pattern is consistent: high cost of failure, plus a small, sharply defined core. railway signalling and interlocking (the B method, Paris Line 14 and other metros) avionics and flight control medical device control security kernels and separation kernels (seL4, proven functionally correct) cryptographic protocol design and verification hardware and processor design — where formal equivalence checking is now completely routine and unremarkable distributed protocol design (TLA+, model-checking consensus and replication protocols) THE MODERN PRAGMATIC POSITION — "LIGHTWEIGHT FORMAL METHODS": do not attempt to prove the whole system. Apply formality where the state space is large and human intuition fails: · MODEL CHECKING a concurrency or distributed protocol, where the interleavings are too numerous to test but few enough for a tool to exhaust · TYPE SYSTEMS as machine-checked lightweight proofs — a strong type system is a formal method that ordinary engineers use daily without noticing · STATIC ANALYSIS and abstract interpretation to prove the absence of specific defect classes (null dereference, buffer overrun, integer overflow) · DESIGN-BY-CONTRACT — preconditions, postconditions and invariants as executable assertions, checked at run time rather than proven. Most of the specification discipline, at a small fraction of the cost, and it is the form of formality most worth adopting in ordinary work. THAT LAST BULLET IS THE PRACTICAL TAKEAWAY: the habit of writing down a precondition, a postcondition and an invariant for each operation captures most of the benefit — the ambiguities surface — without requiring anyone to construct a proof.