This graduate-level text provides an introduction to software
specification emphasizing formal methods that are relevant to
requirements and design stages of software development. The book can
also be used as a text for a one-semester course on formal methods at
the senior undergraduate level. Readers are assumed to have a working
knowledge of software engineering and basic discrete mathematics, but
otherwise this may be their first encounter with formal specification.
It is based on graduate courses and courses offered to professionals
working in the software industry. The authors emphasize the need for
formal abstraction in specification and the advantages it confers on the
software process. In addition, the book covers three major specification
languages: Larch, VDM and Z in some depth. Consequently, readers will be
able to select a formal method that best suits their needs and
The first part of the book discusses specification in general and the
abstraction process. Next comes chapters on the mathematical required.
Third, the authors develop a chapter each to the three major
specification languages, with a number of examples and a case study to
illustrate the expressive power of each language.