The B-book

by Jean-Raymond Abrial

The B method is a means for specifying, designing and coding software systems. The long-awaited B-Book is the standard reference for everything concerning this method. It contains the mathematical basis on which it is founded, the precise definitions of the notations used, and a large number of examples illustrating its use in practice. J-R Abrial, the inventor of B, has written the book in such a way that it can be used for self-study or for reference. It is in four parts, the first dealing with the mathematical foundations, including a systematic construction of predicate logic and set theory, and the definition of the various mathematical structures that are needed to formalise software systems; special emphasis is placed on the notion of proof. The second part contains a presentation of the Generalised Substitution Language and of the Abstract Machine Notation, which are both used to specify software systems; examples are given to show how large specifications can be constructed sy