B - hold the future of software development

The field of formal methods, the application of mathematically based techniques to the specification and development of computer-based systems, has been evolving for several decades.

Alan Turing's contribution to the subject in the middle of the 20th century was very mathematically based and included work on proving programs correct. Tony Hoare's 1969 paper on "An axiomatic basis for computer programming" was perhaps a pivotal point that inspired much subsequent research and provided us with Hoare logic, specifically for reasoning about programs.

In the 1970s, Jean-Raymond Abrial started to consider the specification of data structures and programs. He visited the Oxford University Computing Laboratory where he initiated the Z notation, described as the Oxford "house style" for the use of predicate logic and set theory in the specification of discrete digital software (and sometimes hardware) systems.

Z has proved to be remarkably popular in certain sections of industry compared to other formal techniques. It is perhaps the most widely used formal specification notation in industry, and is taught on many computer science undergraduate courses, especially in the United Kingdom and in continental Europe. However, while Z is an excellent notation, once thoroughly learned, for formal specification, it is not so good for the development part of the design process. It is possible to "refine" a Z specification part way towards an implementation, but mechanised tool support is not good and there is always the necessary but problematic jump to the program code itself to be considered.

Often benefits can be gained from formal specification alone, by discovering errors earlier in the design cycle when they are cheaper to correct. For greater assurance, as required in many critical areas including safety-critical systems, it is worth using a mathematical approach to the program development process as well as the specification itself. For such systems, Abrial and others have developed the B-Method, with associated machine support from the B-Tool. The specification notation used, AMN or Abstract Machine Notation, is Z-like. However, it is designed to allow tool-supported development of a specification in AMN all the way down to executable programs. The "schema" structuring technique of Z, where mathematical fragments of specification are captured and combined in schema boxes, has been replaced with the concept of abstract machines which allow pseudo-program specifications (which are normally not executable directly) to be transformed into real programs more conveniently.

The book is the culmination of more than a decade on the development of B by the author and his collaborators, and more than two decades considering a mathematically rigorous approach to software specification and development. It will act as the reference book for many involved in the application of the B-Method. The approach is increasingly being used in industry and taught on some computer science undergraduate curricula. It has been used to develop real critical systems. Perhaps the best known example of the use of B is the development of the Paris Metro braking system software. Here the choice was between reducing the timing between trains by increasing the assurance in the system as a whole, or building a new tunnel at vast cost. It was worthwhile spending a significant amount of money on ensuring the system worked correctly.

It has now been demonstrated that it can be commercially feasible and worthwhile to prove correct programs of the order of several tens of thousands of lines of code (using B). While this is not large in absolute terms it is sufficient for many critical applications where it is advantageous to restrict the size and complexity of the code for safety reasons.

The B-Book provides a comprehensive reference for the B approach to specifying, designing, and coding software systems. It is split into four major parts: mathematics (set theory and predicate logic with definitions for helping the formalisation of software systems); abstract machines (on the Generalised Substitution Language of B as well as AMN for the specification of software systems); programming (on control structures and systematic construction of algorithms); and refinement (for development of specifications into programs).

This book is technically detailed and comprehensive, covering the mathematical foundations and the more practical details of using B. A guide is provided in how readers, from theoretical computer scientist to industrial practitioner, and with different goals can approach the book. For undergraduates there are other more introductory textbooks on B which may be more suitable.

This book is for the professional software engineer or researcher, be it in industry or academia. The subtitle "Assigning programs to meanings" may puzzle some in the computer world. Many are forced to spend their time attempting to assign meanings to programs, which is a reverse engineering approach to software maintenance that should only to be undertaken when programs exist that have no meaningful specification. Unfortunately this is often the case for many existing programs. This book should help to ensure that some future programs do not suffer the same problems. Indeed, approaches such as B allow the possibility of undertaking software maintenance much more at the specification level rather than the program level. Given that specifications are much less complex than their matching programs, this has the cost-saving potential of helping to simplify maintenance.

Any successful development approach takes at least a decade from conception to actual use in industry. The B-Method has now reached this stage and I hope the publication of this book will act as a milestone in the practical application of B. I look forward to monitoring its journey in the industrial world with interest.

The B-Book is not for the faint-hearted, but will repay the effort invested in digesting its serious message for the software development community.

Jonathan Bowen is a lecturer in computer science, University of Reading. For further information on the B-Method, see http://www.comlab.ox.ac.uk/ archive/formal-methods/b.html