Book excerpts:

Although young by the standards of most engineering disciplines, software development tackles tasks of enormous complexity. In seeking a systematic approach to control this complexity, the software industry is recognizing the need for a variety of new practices. High on their list is an acceptance that formal methods are necessary if large systems are to be developed to higher standards than currently prevail. Formal methods is a term which is used to cover both the use of mathematical notation in the functional specifications of systems and the use of justifications which relate designs to their specifications.

This book covers the case studies on the application of the most widely known and used formal methods in software development, called the Vienna Development Method (more often referred to as VDM). VDM was developed in an industrial environment but has also evoked considerable academic research.

VDM provides both a specification notation and proof obligations which enable a designer to establish the correctness of steps of design. It is a development method in the sense that it offers notation and framework for recording and justifying specifications and design steps. VDM does not, however, claim to be a normative method in the sense that it results in the choice of a standard or best design: the designer provides the insight.

One difficulity faced by many authors of VDM literatures, is to convey their own experiences in describing major computer systems using methods like VDM. Although the examples in this book are not large by industrial standards, they should provide a much clearer indication of how to tackle major systems than is possible in any book whose main task is teaching the method from scratch. Thus, to lead steps desribed in this book examples to an industry-sized specification has to be bridged by some sort of case study.

While there are ten authors in this book who contributed to a total of twelve case studies, the reader must become aware that there is often no 'right' specification. Furthermore, seeing a range of styles will help the readers focus on what they wish to develop as their own approach.

Different users of this book will obviously employ it in different ways. It is likely to be background reading for undergraduate courses which use one or the other textbook to teach VDM; while an MSc or industrial course might make detailed analysis of the case studies. A particularly valuable way of doing this is to organize some sort of 'walk­through' of chosen examples. By their very nature, few of the examples are closed and there is excellent scope for extending a case study as a major project.