The B-Technologies: A System for Computer Aided Programming

Dave S. Neilson
Ib Holm Sørensen

In 6th NWPT, pages 18-35

Abstract:

The paper introduces the B-Technologies, a mathematically based formal method and a tool-set for computer aided software engineering.
The B-Technologies (comprising three components - the B-Method, the B-Tool and the B-Toolkit) have been designed to scale up formal methods for practical application. The B-Method and the B-Toolkit are described in this paper.
The B-Method is designed to provide a notation and a methodology for the formal specification, design, implementation and maintenance of industrial-scale software systems. The features of incremental construction of layered software as well as its incremental verification have been guiding principles in the development of the B-Method. The method uses J-R Abrial's Abstract Machine Notation (AMN) as the language for specification, design and implementation within the software process. AMN is is based on an extension of Dijkstra's guarded command notation, with built-in structuring mechanisms for the construction of large systems.

The B-Toolkit supports the method over the entire spectrum of activities from specification through design and implementation into maintenance. The B-Toolkit comprises automatic and interactive theorem-proving assistants, a proof printer and a set of software development tools: an AMN syntax & type checker, a specification animator and generators promoting an object oriented approach at all stages of development, and the re-use of specification models/software modules. All tools are integrated with the proof assistants into a window-based development environment.

Comments
B-Core Limited, Magdalen Centre, Oxford Science Park, Oxford OX4 4GA, United Kingdom. Email: {Dave.Neilson,Ib.Sorensen}@comlab.ox.ac.uk.

Available as PostScript, DVI.

BRICS WWW home page