Reference:

B-hold the Future of Software Development. The Times Higher Education Supplement, Multimedia computer books, 1267:30, 14 February 1997. Review of The B-Book: Assigning Programs to Meanings, J.-R. Abrial, Cambridge University Press, 1996.

B-hold the Future of Software Development

The field of

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, which has been 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 now taught on many computer science undergraduate courses, especially in the UK 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 mechanized 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 many errors earlier on in the design cycle when they are much cheaper to correct. However, for even greater assurance as required in many critical systems, such as in safety-critical areas where human lifes are at stake, 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 a method, known as 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 of effort on the development of B by the author and his collaborators, and more that two decades of effort in 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 being increasingly used in industry and is now taught on some computer science undergraduate curricula. It has been used to successfully develop real critical systems.

Perhaps the most well known example using 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. Thus 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 - large programs are of the order of tens of millions of lines of code - 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 for major parts, Mathematics (set theory and predicate logic with definitions to helping the formalization of software systems), Abstract Machines (on the Generalized 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 both the mathematical foundations and the more practical details of using B. A helpful guide is provided in how readers of different backgrounds (from theoretical computer scientist to industrial practitioner) and with different goals can approach the book. For undergraduates there are now 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 today. Hopefully this book will help to ensure that some programs of tomorrow 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 potential of helping to simplify the maintenance process, which is normally the dominant part of the cost of a program during its lifetime.

Any successful development approach takes at least a decade, and often more, 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. As Prof. Tony Hoare says in the tribute at the beginning of the book, ``Read, learn, enjoy and prosper!''

For further information on the B-Method, including information on this and other B books, see the entry in the Virtual Library formal methods online information under:

Note: The text above is as originally submitted to the Times Higher Education Supplement, and has been copy edited in the final published version. It may be reproduced for non-commercial purposes if full acknowledgement to the author and publisher are given.