Investigation of the B Method

The B method as a mathematical concept with its underlying theories will be presented. The presentation will follow a review of the historical devel-opment in formal program specification. The presentation of the B method will be structured into the Abstract Specification, Refinement and Imple-mentation of a development. Concepts will be illustrated by short examples. In particular, proof obligations of B machines will be presented and briefly explained. Alongside, the design methodologies Bottom-up and Top-down in respect to structuring a B development will be discussed. Further, the B-Toolkit as a software tool to assist B developments will be presented with its most important facilities. Special interest will be given to the proof mecha-nisms of the B-Toolkit. A development example of the board game “Noughts & Crosses ” will be performed to illustrate the theoretical concepts as they have been presented in the previous chapters. The development will include specification, implementation and complete discharge of all consistency proo