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. 1 Introduction.- 1.1 Formal Methods.- 1.2 The History of B.- 1.3 The Relationship of B to Other Formal Methods.- 1.4 Summary.- 2 The Foundations of B AMN.- 2.1 Mathematical Notation.- 2.2 Defining Operations.- 2.3 Abstract Machines.- 2.4 Machine Composition Mechanisms.- 2.5 Refinement.- 2.6 Implementation.- 2.7 Summary.- 2.8 Exercises 1.- 3 Analysis and Specification.- 3.1 Requirements Analysis.- 3.2 Specification Development.- 3.3 Animation.- 3.4 Proof of Internal Consistency Obligations.- 3.5 Ship Loading Case Study - Specification.- 3.6 Renaming.- 3.7 Aggregation.- 3.8 Summary.- 3.9 Exercises 2.- 4 Design and Implementation.- 4.1 The Layered Development Paradigm.- 4.2 Refinement Examples.- 4.3 Proofs of Refinement.- 4.4 Decomposing Implementations.- 4.5 Ship Loading Case Study - Implementation.- 4.6 Summary.- 4.7 Exercises 3.- 5 Case Studies.- 5.1 Personnel System Development.- 5.2 Mine Pump Control.- 5.3 Vending Machine.- 6 Conclusions.- A Exercise Solutions.- A.1 Exercises 1.- A.2 Exercises 2.- A.3 Exercises 3.- B Properties of Weakest Preconditions.- B.1 Termination and Feasibility.- B.2 Set-theoretic Semantics.- B.3 Refinement.- B.4 Well-formedness Obligations.- B.5 Normal Forms.- B.6 Rules for ?.- B.7 Definition of :=.- C Proof Techniques.
