Proof and refutation: a universal interface claim dies on one counterexample

Many design-review sentences sound like taste. They are claims about sets. "Every action can be undone." "No screen is more than four taps from home." "The device cannot deliver a dose unless the operator has confirmed it." Each sentence describes a space of states. It is true of the whole space or false of at least one corner of it. The mathematics begins before the proof, in the quantifier.

This unit argues that the shape of the quantifier decides what formal work is worth doing. One counterexample refutes a universal claim, so the cheapest useful act of reasoning about an interface is a search for a counterexample rather than a proof. Formal proof then earns its cost where a false claim is fatal. Unit 2 supplies the object such claims are about, which is the next-state map.

A design claim is a claim about a set

Take the sentence "every action can be undone". Written out, it says that for every state the interface can reach, there is a sequence of inputs that returns the user to where they started. Its negation says that there is at least one state from which no such sequence exists. One witness settles the negation. Only the whole space settles the claim. An existential claim behaves the other way round: "there is a way to export the record" is established by one trace and refuted only by exhausting the space.

A drawing application makes the asymmetry concrete. In the model, every stroke can be undone, because every mutation pushes onto an undo stack. On the machine, closing the document drops the stack. So the state reached by pressing close and then reopen has no sequence of inputs returning the user to the unsaved stroke. The counterexample is two inputs long. The claim holds of the abstraction and fails on the artefact. The claim also ranges over people. "Every action can be undone" is quantified over all who can operate the interface, so the decisive witness may be a user the designer did not picture. Offer a control to a pointer but not to an assistive technology, and the state is reachable while the sequence out of it is not, because the input alphabet is part of the model.

Therac-25: a witness that should have ended the claim

The Therac-25 is the worked case, and Leveson and Turner's 1993 investigation is its record. They reconstructed events from interviews, depositions and regulatory correspondence, describing six radiation overdoses on a computer-controlled linear accelerator between June 1985 and January 1987, and arguing that the accidents were system accidents rather than the failure of a single component. After the first accident the manufacturer modified the machine. It claimed that the redesign had improved safety by at least five orders of magnitude. That is a universal claim about the new device.

In December 1985 a patient at Yakima suffered a striped skin burn. The manufacturer did not treat it as a counterexample. In February 1986 it wrote that the damage could not have been produced by any malfunction of the machine. A witness existed and was known. It did not end the claim. A counterexample only refutes a statement that someone is willing to regard as the statement. The logic is cheap; the social act of accepting the witness is not.

The paper records a harder lesson for anyone who wants refutation to be mechanical: a later incident took a medical physicist who searched for a keystroke sequence he could not at first repeat, and converting an injury into a reproducible trace took equipment and patience. It is the trace, not the injury, that a tool can consume.

One instrument proves a claim, the other returns a witness

Formal work on interfaces descends from two instruments that do different jobs, the first being proof. Hoare's 1969 axioms and rules of inference let a program's properties be proved rather than asserted. The specification is written as a precondition and postcondition, which makes the obligations visible. The second instrument is the mechanised search for a witness. Clarke and Emerson's 1982 procedure represents a finite-state system as a Kripke structure. It decides a branching-time temporal formula against that structure. Where the formula does not hold, it returns the path that violates it. Refutation becomes a computation rather than an argument.

Their worked case was a synchronisation skeleton: two processes competing for a shared resource, checked for mutual exclusion, and the procedure returned the interleaving that violates it, which is what a designer can read. It is a model of processes, and a person appears in it only if someone puts them there.

Wing's 1990 survey fixes the tradition's vocabulary, covering mathematically based techniques for describing system properties across six illustrated methods including Z, VDM, Larch and CSP.

Proof pays only where failure is unacceptable

When is proof worth buying? Bowen and Hinchey argued in 1995 that formal methods pay where failure is unacceptable and are resisted through misconceptions about cost, giving ten maxims whose first is that the justification is consequence, not elegance. Revisiting them in 2006, they found adoption improved only at the margins, with the cost of the mathematics still the obstacle. Woodcock and colleagues' 2009 survey is narrower still. Projects concentrated on specification and design, appeared where regulation or consequence forced the issue, and kept adoption uneven because of engineering obstacles.

The clearest modern case is the Meteor line 14 of the Paris Metro, which opened driverless in October 1998 with its safety-critical automatic train protection developed in the B method (Behm and colleagues, 1999). The project team reports over 110,000 lines of B model translated into 86,000 lines of Ada, with no bug detected once the proofs were complete (Lecomte and colleagues, 2020). Consequence justified the cost, and the assurance came from proof rather than testing. It does not transfer to an interface: that argument concerned doors, trains and track sections, whose state is discrete and whose behaviour is regulated, and a claim such as "every action can be undone" carries no certificate of that kind.

The claim is usually wrong before it is unproved

A second reason may put the proof on the wrong target, since Nuseibeh and Easterbrook's 2000 requirements roadmap identifies the central difficulties of requirements work: modelling the problem domain rather than software behaviour, non-functional requirements, and the gap between contextual enquiry and formal specification, whose bridging it names as an open problem. If that is right, the failure this unit cares about is upstream of the proof: the claim is not misproved, it is wrongly written down.

Parnas and Clements had made the historical case in 1986: a design cannot in practice be derived from a fixed statement of requirements, though the documentation such a derivation would have produced can be reconstructed afterwards. Read against the thesis, their point is that the specification is a reconstruction rather than a record: written invariants no tool enforces, valued because writing a claim down is what makes it attackable.

A claim about an interface needs the person inside the model

None of this is confined to protocols. Campos and Harrison showed in 2001 how an interactor-style specification can be compiled into a finite-state model and checked against usability and task properties, the checker returning counterexample traces.

Bolton and Bass carried the machinery to a person-plus-interface system in 2009, integrating task-analytic models of operator behaviour with a formal model and model checking on a patient-controlled analgesia pump. Of two specifications checked, one returned a counterexample and the path that violated it. The human's procedure is inside the model, which is what makes the claim about the interface rather than the code.

Contested question: what does a proof certify?

The disagreement is about the object of proof. Fetzer argued in 1988 that verification trades on an equivocation. Algorithms as logical structures suit deductive proof, while programs as causal devices do not, so a proof can never guarantee a running machine. His case is an argument from the nature of the object rather than a measurement, and it has been answered in detail rather than refuted in kind. Rushby's 1997 reply is the sharpest: a certification authority accepts a formal development for the rigour of the argument it carries.

The empirical weight sits on the other side, and its strength is easier to grade: Hoare's axioms and Clarke and Emerson's procedure are constructive, since they show the obligations can be written and the violating path found. The strongest field case is the Meteor line, where a proved specification preceded a service record free of failure attributed to the proved code (Behm and colleagues, 1999; Lecomte and colleagues, 2020). That case is one project team reporting its own outcome. Campos and Harrison's interface revision and Bolton and Bass's pump case are single worked examples.

The other position is that the model is chosen so that its failures are real, so the value of the formality lies in what it makes explicit.

What would settle it is a published count of how many model counterexamples reproduce on the artefact. The Therac-25 investigation is the closest case, its path reconstructed from the machine rather than derived from a model (Leveson and Turner, 1993). Until such a count exists, Fetzer's position is a caution rather than a veto.

Meanwhile, treat the model as the claim under review and the machine as the evidence, record for every witness the assumption that makes it real, write the invariant where a false claim would be embarrassing, and buy the search where it would be fatal.

Where the argument is heading

The direction of travel is to make refutation cheap and leave proof expensive on purpose. Jackson presented Alloy in 2002 as a small relational modelling language whose analyser searches a bounded scope for counterexamples. The method is partial by design: it refutes a claim that fails in a small model and cannot prove a general one. Silvis-Cividjian's 2024 article revisits the Therac-25 four decades on, asking why comparable failures recur. The agenda is to build tools that find small witnesses, and to ask whether the trace found is the trace that would have saved the patient.

The sources this unit rests on

• Leveson, N. G. and Turner, C. S. (1993). An investigation of the Therac-25 accidents. Computer, 26(7), 18-41. doi:10.1109/MC.1993.274940 Reconstructs six overdoses on a computer-controlled linear accelerator, arguing they were system accidents. The paper records a claimed five-orders-of-magnitude improvement and a refused counterexample.
• Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12(10), 576-580. doi:10.1145/363235.363259 Axioms and inference rules let a small language's properties be proved rather than asserted, worked on a simple theorem: the origin of the interface claim as a proof obligation.
• Clarke, E. M. and Emerson, E. A. (1982). Design and synthesis of synchronization skeletons using branching time temporal logic. Lecture Notes in Computer Science, 131, 52-71. doi:10.1007/BFb0025774 Introduces the algorithmic core of model checking, deciding a temporal-logic formula against a finite-state structure and returning the violating path.
• Wing, J. M. (1990). A specifier's introduction to formal methods. Computer, 23(9), 8-22. doi:10.1109/2.58215 Defines formal methods and surveys six specification methods, including Z, VDM and Larch, alongside the objections practitioners raise.
• Bowen, J. P. and Hinchey, M. G. (1995). Ten commandments of formal methods. Computer, 28(4), 56-63. doi:10.1109/2.375178 Argues that formal methods pay where failure is unacceptable and are resisted because of misconceptions about cost, with ten maxims.
• Bowen, J. P. and Hinchey, M. G. (2006). Ten commandments of formal methods ... ten years later. Computer, 39(1), 40-48. doi:10.1109/MC.2006.35 Revisiting the maxims, the authors find adoption improved only at the margins, with the cost of the mathematics still the obstacle.
• Behm, P., Benoit, P., Faivre, A. and Meynadier, J.-M. (1999). Meteor: a successful application of B in a large project. FM'99, Lecture Notes in Computer Science 1708, 369-387. doi:10.1007/3-540-48119-2_22 The industrial project behind the Paris Meteor line 14, where safety-critical parts of the automatic train control were specified and proved in B. The real case for the unit's condition on cost.
• Lecomte, T., Deharbe, D., Prun, E. and Mottin, E. (2020). Applying a formal method in industry: a 25-year trajectory. arXiv:2005.07190. https://arxiv.org/abs/2005.07190 Reports twenty-five years of B and Event-B in industry and gives the Meteor figures: over 110,000 lines of model translated into 86,000 lines of Ada, no bug detected in validation, on site or in operation since 1998. The figures are the project team's own report.
• Woodcock, J., Larsen, P. G., Bicarregui, J. and Fitzgerald, J. (2009). Formal methods: practice and experience. ACM Computing Surveys, 41(4), 1-36. doi:10.1145/1592434.1592436 Surveys industrial use against earlier surveys over twenty years, with projects concentrated on specification and design.
• Nuseibeh, B. and Easterbrook, S. (2000). Requirements engineering: a roadmap. Proceedings of the Conference on the Future of Software Engineering (ICSE). doi:10.1145/336512.336523 Names the central difficulties of requirements work, including modelling the problem domain and the gap to formal specification.
• Parnas, D. L. and Clements, P. C. (1986). A rational design process: how and why to fake it. IEEE Transactions on Software Engineering, SE-12(2), 251-257. doi:10.1109/TSE.1986.6312940 Argues that a design cannot be derived from fixed requirements, though the documentation such a derivation would have produced can be reconstructed.
• Campos, J. C. and Harrison, M. D. (2001). Model checking interactor specifications. Automated Software Engineering, 8(3-4), 275-310. doi:10.1023/A:1011265604021 Compiles an interactor-style interface specification into a finite-state model and checks task properties such as reachability and reversibility.
• Bolton, M. L. and Bass, E. J. (2009). A method for the formal verification of human-interactive systems. Proceedings of the Human Factors and Ergonomics Society Annual Meeting, 53(12), 764-768. doi:10.1518/107118109X12524442637309 Integrates operator task models with model checking on a patient-controlled analgesia pump, one specification returning a counterexample.
• Fetzer, J. H. (1988). Program verification: the very idea. Communications of the ACM, 31(9), 1048-1063. doi:10.1145/48529.48530 Argues that verification equivocates between algorithms as logical structures fit for proof and programs as causal devices that are not.
• Jackson, D. (2002). Alloy: a lightweight modelling language. ACM Transactions on Software Engineering and Methodology, 11(2), 256-290. doi:10.1145/505145.505149 Presents Alloy, whose analyser searches a bounded scope for counterexamples, and reports cheap defect finding.
• Silvis-Cividjian, N. (2024). Therac-25 accidents: we keep on learning from them. Computer, 57(12), 69-78. doi:10.1109/MC.2024.3450197 Revisits the Therac-25 four decades on, asking what the investigation established and why comparable failures recur. The published counterexample did not end the class of failure.