Foreword
The
formal methods community
has, in writing about the use of discrete mathematics for system
specification, committed a number of serious errors. The main one is
to concentrate on problems which are too small, for example it has
elevated the stack to a level of importance not dreamt of by its
inventors. While there is a good reason for using small examples at the
beginning of a book or a tutorial, the need becomes progressively less
important as one progresses towards teaching students and industrial
staff topics such as structuring and modelling. Too many books have
given up the fight after presenting small examples and have, I believe,
contributed greatly to the lack of take-up of this technology. Staff
and students who have read introductory materials on formal methods
such as Z and
VDM have had their hopes
raised by small examples which have given the impression that formal
specification is merely the writing down of some simple mathematical
statements which define the behaviour of a system. What small examples
do is to hide one of the most difficult tasks of specification: the
process of selecting an adequate model.
Jonathan Bowen is a formal methods researcher who I have a great
deal of respect for. Almost all his work has concentrated on the
application of this technology to real-life problems - not just stacks
and queues. His book teaches through the medium of case studies which
are realistic but not too large that they overwhelm the reader. They
range from the specification of the Transputer instruction set to that
of a tool for formatting free text. All the case studies contain
excellent examples of the power of Z: its ability to structure large
specifications into chunks which can be read, validated and developed
in relative isolation.
The formal methods community still have a long way to go in convincing
many industrialists of the power of discrete mathematics; I would
regard this book as a major contribution to doing so.
Darrel Ince
Computing Department,
The Open University