II/2/1/6 The B Method Course

The B Method: An Overview

The B method is the result of the inspirational work of Jean-Raymound Abrial, who developed it with a team of researchers at BP Sunbury in the later 1980s. It is a formal approach to the specification and development of computer software systems. B draws together advances in the formal methods that span the last thirty years, including the Z notations, pre and post conditions, guarded commands, stepwise refinement, refinement calculus and date refinement. It synthesises them into a unified pragmatic and usable development methodology.
The method is based on a wide-spectrum pseudo-programming notation, the Abstract Machine Notation (AMN), which provides a common framework for the construction of specifications, refinements and implementations. AMN provides structuring mechanisms which support modularity and abstraction in an object-based style, making provable correctness a realistic and achievable goal. The method is based around the concept of layered development, which builds larger components from collections of smaller ones.
The B method essentially deals with the central aspects of the software life cycle, namely: the technical specification, the design by successive refinement steps, the layered architecture, and the executable code generation. Each of the previous items is envisaged as an activity that involves writing mathematical proofs in order to justify its results. It is, the collection of such proofs that makes one convinced that the software system in question is indeed correct.
A software system conceived with the method is composed of several abstract machines. Each machine contains some data and offers some operations. The data cannot be reached directly; they are always reached through the operations of the machine.
Each operation of an abstract machine is described as a pre-condition and an atomic action, which does not contains any sequencing or loop. The pre-condition expresses the indispensable condition without which the operation cannot be invoked. The atomic action is formalised by means of a generalised substitution.
The initial model of an abstract machine may be refined in an executable module. This passage from specification to code is carried out entirely controlled by the method. It is thus necessarily concluded by some proofs, whose goal is to show that the final code of a machine indeed satisfies its specification.
The course assumes no prior knowledge of formal methods or of reasoning about program. A previous exposure to logic and set theory would be an advantage though it is not essential: the course assumes a basic ability to manipulate simple logic and set theoretic expressions.
Course Contents
1. Introduction
1.1 Set notations
1.2 Mathematical objects

2. Abstract machines
2.1 Specifying the state
2.2 Specifying the operations
2.3 Substitution as specification

3. Formal definition of abstract machines
3.1 Generalised substitutions
3.2 Proof obligations
3.3 Type-checking

4. Constructing large abstract machines
4.1 Multiple generalised substitution
4.2 Incremental specification and sharing

5 Refinement
5.1 Refinement of generalised substitutions
5.2 Refinement of abstract machine

6. Constructing large software systems
6.1 Implementing a refinement
6.2 Sharing
6.3 Multiple refinement and implementation

7. Examples
7.1 An invoice system
7.2 A lift control system
7.3 A port management system
References
1. J-R Abrial: The B Book, Cambridge University Press, (1996)
2. J. Woodcock and M. Loomes: Software engineering mathematics, Pitman, (1988)
3. C.C. Morgan: Programming from specifications, Prentice Hall, (1994)
4. J.M. Spivey: The Z notations: a reference manual, Prentice hall, (1992)
5. E.W. Dijkstra: A discipline of programming, Prentice hall, (1976)
6. R.J.R. Back and J. von Wright: Refinement calculus, LNCS 430, 42-66, (1989)
7.He Jifeng, C.A.R. Hoare and J. Sanders: Data refinement refined, LNCS 213, 187-196, (1986)
8. C.B. Jones: Systematic software development using VDM, Prentice hall, (1986)
9. J.M. Morris: A theoretical basis for stepwise refinement, Science of computer programming, (1986)
10. S. Schneider: THe B method: an introduction, Palgrave, (2001)

iistinfo@iist.unu.edu,

The B Method Course

Software Project Management Course

Course Descriptions

Model Checking Course

UNU-IIST Home