The B-Method

The B-Method is a collection of mathematically based techniques for the specification, design and implementation of software components. Systems are modelled as a collection of interdependent Abstract Machines, for which an object-based approach is employed at all stages of development.

An Abstract Machine is described using the Abstract Machine Notation (AMN). A uniform notation is used at all levels of description, from specification, through design, to implementation.

AMN is a state-based formal specification language in the same school as VDM and Z. An Abstract Machine comprises a state together with operations on that state. In a specification and a design of an Abstract Machine the state is modelled using notions like sets, relations, functions, sequences etc.. The operations are modelled using Pre- and Post-conditions using AMN.

In an implementation of an abstract machine the state is again modelled using a set-theoretical model, but this time we already have an implementation for the model. The operations are described using a pseudo-programming notation that is a subset of AMN.

The B-Method prescribes how to check the specification for consistency (preservation of invariant) and how to check designs and implementations for correctness (correctness of data refinement and correctness of algorithmic refinement).

The B-Method further prescribes how to structure large designs and large developments, and promotes the re-use of specification models and software modules, with object orientation central to specification construction and implementation design.

A great deal of attention has been paid to making the notational aspect of the method as simple as possible. To the engineer, the formal notation looks like a simple pseudo programming notation. And as mentioned above, there is no real distinction between the specification notation and the programming notation.

The method and the notation have been designed together with the B-Toolkit that supports them, so that every aspect of the method has been validated by the possibility of providing significant help to the engineer in using computer based tools to write, verify and maintain software. Most theoretical aspects of the method, such as formulation of proof obligations, are done automatically by the tools. The provers are also designed to run automatically and reference a large library of mathematical rules, provided with the system.

Separate (object based) techniques within the method support the design of (large) specification construction and that of (large) program construction. The complex dependencies within such big systems are automatically controlled by the tools.

A full on-line help listing is available in the Contents Page Also available in the form of a complete Index. Blogo