This book provides a textbook introduction to the B-Method, a rigorous methodology for the development of correct software. The text covers all stages of the B software development process - from specification, through refinement and design, down to implementation and automatic code generation. The method uses a single uniform notation throughout development, designed to enable verification at each stage whilst placing particular emphasis on correctness.
* Suitable for undergraduate and postgraduate courses on formal methods and software development
* Written in a clear tutorial style of explanation
* Contains numerous illustrative examples, exercises and self-testing questions with solutions throughout
* Relevant to users of any B-Method CASE tool
* Teaching materials available online
The B-Method : An Introduction also offers readers powerful tool support by providing a free licence for the B-Toolkit - an integrated toolset which supports and extends the entire B development lifecycle.
STEVE SCHNEIDER is Professor of Computing in the Department of Computing, University of Surrey, UK. He has taught the B-method at undergraduate and postgraduate level over a number of years, and has published papers on B at international formal methods conferences and workshops.
Preface.- Introducing Abstract Machines.- Review of Set Theory and Logic.- Weakest Preconditions.- Towards Machine Consistency.- Parameters, Sets and Constants.- Relations.- Functions and Sequences.- Arrays.- Nondeterminism.- Structuring with INCLUDES.- Structuring with SEES and USES.- Data Refinement.- Refinement of Nondetermnism.- Proof Obligations for Refinements.- Loops.- Implementation Machines.- Case Study: Heapsort.- Library Machines.- Answers to SelfTests.- Appendix A: Generalised Substitution Language.- Appendix B: Machine Readable AMN .- Index.- Index of Machines.