The B Language and Method: A Guide to Practical Formal Development
This book is published
by Springer-Verlag
in the FACIT series.
It provides a detailed introduction to specification and
refinement in B. The history of development of B is covered,
together with the mathematical underpinnings of the notation.
Particular emphasis
is placed on the use of B in the context
of existing software development methods, including object-oriented
analysis and design. Specifically designed to support the teaching of B
at undergraduate and postgraduate level, the text includes a
large number of worked examples and graduated
exercises in B AMN specification.
It also includes two extended case studies of
the development
process, and an appendix of proof techniques suitable for B.
Contents
- Introduction: Formal Methods, History of B, relationship with
other methods
- The Foundations of B AMN: Mathematical notation, operations, machines,
machine composition, overview of refinement and implementation
- Analysis and Specification: Mapping analysis models into B, validation
via animation
- Design and Implementation: Layered development paradigm,
implementation decomposition
- Case Studies
- Appendix A: Weakest preconditions
- Appendix B: Proof techniques
A glossary, index and bibliography are provided.
Author : Kevin Lano has been involved in the development
and application of VDM++ and Z++,
and
is the author of a number of papers and books
in the field of formal methods.
He has used B for industrial software specification, and teaches a
course on B at
Imperial College.
Length : 236 pages.
Cost : 29.50 UK pounds.
How to Order
Due: May 1996.
ISBN: 3-540-76033-4
Springer-Verlag London Ltd.,
Sweetapple House,
Catteshall Rd.,
Godalming,
Surrey.
GU7 3DJ.