Lightweight formal methods

Daniel Jackson and Jeannette Wing
School of Computer Science
Carnegie Mellon University

Many of the benefits promised by formal methods are shared with other approaches. The precision of mathematical thinking relies not on formality but on careful use of mathematical notions; you don't need to know Z to think about sets and functions. Likewise, the linguistic advantages of a formal notation rely more on syntax than semantics.

Mechanical analysis, in contrast, is a benefit unique to formal approaches. An engineer's sketch can communicate ideas to other engineers, but only a plan can be rigorously examined for flaws. Informal methods often provide some analysis too, but since their notations are generally incapable of expressing behaviour, the results of the analysis bear only on the properties of the artifact's description, and not on the properties of the artifact itself.

For everyday software development, the purpose of formalization is to reduce the risk of serious specification and design errors. Analysis can expose such errors while they are still cheap to fix. Formal methods can provide limited guarantees of correctness too, but, except in safety-critical work, the cost of full verification is prohibitive and early detection of errors is a more realistic goal.

To make analysis economically feasible, the cost of specification must be dramatically reduced, and the analysis itself must be automated. Experience (of several decades) with interactive theorem proving has shown that the cost of proof is usually an order of magnitude greater than the cost of specification. And yet the cost of specification alone is often beyond a project's budget. Industry will have no reason to adopt formal methods until the benefits of formalization can be obtained immediately, with an analysis that does not require further massive investment.

Existing formal methods, at least if used in the conventional manner, cannot achieve these goals. By promoting full formalization in very expressive languages, they have guaranteed that the benefits of formalization are spread very thin. A lightweight approach, which, in contrast, emphasizes partiality and focused application, can bring greater benefits at reduced cost. What are the elements of a lightweight approach?

Partiality in language. Until now, specification languages have been judged primarily on their expressiveness, with little attention paid to tractability. Some languages ñ such as Larch ñ were from the start designed with tool support in mind, but they are the exception. Tools designed as an afterthought can provide only weak analysis, such as type checking. The tendency (in Z especially) to see a specification language as a general mathematical notation is surely a mistake, since such generality can only come at the expense of analysis (and, moreover, at the expense of the language's suitability for its most common applications).

Partiality in modelling. Since a complete formalization of the properties of a large system is infeasible, the question is not whether specifications should focus on some details at the expense of others, but rather which details merit the cost of formalization. The naive presumption that formalization is useful in its own right must be dropped. There can be no point embarking on the construction of a specification until it is known exactly what the specification is for; which risks it is intended to mitigate; and in which respects it will inevitably prove inadequate.

Partial analysis. A sufficiently expressive language, even if designed for tractability, cannot be decidable, so a sound and complete analysis is impossible. Most specifications contain errors, and so it makes more sense to sacrifice the ability to find proofs than the ability to detect errors reliably. A common objection to this approach is that it reduces analysis to testing, since one can no longer infer from the omission of reported errors the absence of actual errors. But this much-touted weakness of testing is not its major flaw. The problem with testing is not that it cannot show the absence of bugs, but that it fails to show their presence.A model checker that exhausts an enormous state space finds bugs much more reliably than conventional testing techniques, which sample only a minute proportion of cases.

Partiality in composition. For a large system, a single partial specification will not suffice, and it will be necessary to compose many partial specifications, at the very least to support some analysis of consistency. How to compose different views of a system is not well understood, and has only minimal support from specification languages, since it does not fit the standard pattern of `whole-and-part' composition.

Much of what we say here is at odds with the conventional wisdom of formal methods. The notion of a lightweight approach is radical, however, only in its departure from a dogmatic view of formal methods that is detached from mainstream software development. In the broader engineering context, the suggestion of pragmatic compromise is hardly new.

A lightweight approach, in comparison to the traditional approach, lacks power of expression and breadth of coverage. A surgical laser likewise produces less power and poorer coverage than a lightbulb, but it makes more efficient use of the energy it consumes, and its effect is more dramatic.