Book excerpts:

The aim of this book is to contribute to the wider use of formal methods in the specication and design of computer systems. VDM (Vienna Development Method) was developed in an industrial environment and is one of the most widely used formal methods. VDM is used in this book because it has achieved a level of maturity and acceptance: it has been taught for many years and has been used in a wide variety of applications. Furthermore, the British Standards Institution (BSI) work on developing a standard for VDM has been one of the stimuli for this revised edition.

This book teaches a particular systematic approach to software development concentrating on the stages from specication through design to implementation. The term formal methods embraces formal specication and veried design. Many aspects of a computer system must be specied including performance and cost. In this book attention is focused on functional specication (i.e. what the system does); the term specication is, however, used below without qualication for brevity.

Formal specications employ mathematical notation in order to achieve both precision and conciseness. A specication should be much shorter than a corresponding implementation. The key to brevity is abstraction. The specification of a system should abstract away issues which relate to implementation rather than to the intended behaviour of a computer system. The meaning of the operations are specied abstractly by recording properties which they should possess. Listing a collection of properties is one way in which a specication can be much shorter than an implementation. Another key technique for making specications more concise than their implementations is to use abstract data objects which match the system being specied. This can be contrasted to the use of data objects which belong to the machine or language on which the system is to be implemented. The latter are the subject of implementations and should be avoided in specications.