USING Z: SPECIFICATION, REFINEMENT AND PROOF By Jim Woodcock and Jim Davies Prentice Hall 452pp, Pounds 18.95 ISBN 0 139 48472 8.
APPLICATIONS OF FORMAL METHODS By Michael Hinchey and Jonathan Brown Prentice Hall 472pp, Pounds 29.95 ISBN 0 133 66949 1
Formal methods is the term computer scientists use to refer to the use of mathematics in system specification and development (although it has never been clear to me why a special term is needed).
In traditional engineering disciplines, designers of complex systems routinely use mathematical notations to specify and reason about the properties of their designs. This enables them to identify problems before expensive production costs are incurred. Yet, despite the fact that software systems (or systems which contain software components) are among the most complex systems ever built, it is very rare for software designers to use any mathematics at all in their specifications and designs.
This means that there is no possibility of reasoning formally about their proposed systems until the program code is created. By this stage a considerable investment of effort has already been made and crucial specification and design faults are difficult and costly to locate and fix.
It has been claimed that this phenomenon is a major cause of the continuing "software crisis" of poor software quality and late delivery. With the increasing use of software in business-critical, and even safety critical applications, the lack of a proper engineering approach seems reprehensible.
In the light of these observations it will therefore come as a surprise to non-software specialists to learn that formal methods have been around for more than 25 years without having made any significant impact on the worldwide community of software developers.
It is fair to say that there are more textbooks on formal methods than there are documented case studies of their use in real applications. In a sense the two new books reviewed here, although both excellent in their own right, highlight some of the reasons for this poor technology transfer.
In fact, formal methods (in various guises) have been proposed since the early 1970s as a potential solution to the software crisis. So why has there been so little take-up of such an obviously good idea? A major reason, in my view, is that that the wrong benefits have been emphasised.
In particular, proponents massively oversold the notion of proof of correctness as the major motivation for using formal methods. The idea was that, with formal methods, you could specify a system in an appropriate formal notation and then prove (in a mathematical sense) that a subsequent implementation of the system was correct (with respect to the formal specification).
Proponents of formal methods argued (often persuasively) that such an approach even circumvented the need for traditional software testing. Thus, formal methods offered a potentially revolutionary change to the way that software was developed and tested. In practice, no complex systems have ever been developed or proved correct in this way. In general it is infeasible to do so.
The other reason why I believe that formal methods have failed to make the impact that they should have done is that the formal notations themselves (of which there are several to choose from) are too difficult for most practising software engineers to use.
In a recent article, leading expert Dave Parnas commented that the formalists who set out to revolutionise software development may have succeeded only in forming new research cliques in computer science.
Despite these problems there is a growing awareness that formal methods (including the existing non-perfect variety) do have an important role to play, even if it is restricted to the specification stage. The very act of producing a formal specification can be beneficial in identifying requirements faults.
The formal specification notation that has been used most widely in this sense is Z, which originated from Oxford University Programming Research Group. It has also gained widespread acceptance within the academic community.
Woodcock and Davies's book is the latest of several textbooks on Z. Woodcock is a leading authority on Z and is also an excellent communicator. Thus, as you would expect, this book is extremely well-written and researched.
Although there is a significant amount of introductory material (sufficient for most Z courses) the ultimate thrust of the book is related to the original motivation for using formal methods: proving correctness. The authors have a mission to show how Z can truly be used not just for specification, but also for refinement and hence verification.
The material is not for the mathematically faint-hearted, but I believe that the authors succeed in their goal. My concern is that few students of this material will ever put into practice the full method described here.
The Z notation also features heavily in the book by Hinchey and Bowen. This is a well edited collection of case studies that will give readers useful insights into practical applications of a range of notations (including VDM, CCS and B-method).
A collection like this is an important milestone for the formal methods community. However, the collection does little to dispel the view that real industrial use of formal methods is extremely rare.
For example, the most convincing case study here is not a software system at all but a microprocessor, while many of the other examples appear not to have been used in earnest.
Ultimately, I feel the desperately-sought technology transfer breakthrough will come only when there is a body of empirical evidence to demonstrate the efficacy of formal methods in economic and quality terms.
There is no real evidence of this kind in either of these books. Hence their usefulness is ultimately dependent on the empirical studies which have only recently begun to appear.
Norman Fenton is professor of computing science, Centre for Software Reliability, City University.