The B language and method

the long version

B is a formal approach to software specification and development based on the Z specification language. It has been successfully applied in industry, and has robust, commercially available tool support for the entire development lifecycle, from specification through to code generation. The B Language and Method provides a comprehensive introduction to the B Abstract Machine Notation, and how it can be used to support formal specification and development of high integrity systems. Beginning with a discussion of the history of B, it builds up a description of the notation from the basic mathematical notation for sets and sequences, through to the structuring mechanisms of the language, and how it supports "programming in the large". 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.