B is one of the few formal methods which has robust,
commercially-available tool support for the entire development lifecycle
from specification through to code generation. This volume provides a
comprehensive introduction to the B Abstract Machine Notation, and to
how it can be used to support formal specification and development of
high integrity systems. A strong emphasis is placed on the use of B in
the context of existing software development methods, including
object-oriented analysis and design. The text includes a large number of
worked examples, graduated exercises in B AMN specification and
development (all of which have been class-tested), two extended case
studies of the development process, and an appendix of proof techniques
suitable for B. Based on material which has been used to teach B at
postgraduate and undergraduate level, this volume will provide
invaluable reading a wide range of people, including students, project
technical managers and workers, and researchers with an interest in
methods integration and B semantics.