The B-Toolkit

The B-Toolkit comprises a suite of fully integrated software tools designed to support a rigorous or formal development of software systems using the B-Method. The tools are accessed through a custom build X Windows Motif Interface, providing full on-line help facilities.

The B-Method uses the notion of Abstract Machines to specify and design software systems. Abstract Machines are specified using the Abstract Machine Notation (AMN) which is in turn based on the mathematical theory of Generalised Substitutions.

The Toolkit also provides a development environment automating the management of all associated files, ensuring that the entire development, including code and documentation, is always in a consistent state. One aspect of this environment is that the effect of change in a single file on the entire system is communicated to the user before the decision is made to commit the change to the system (this information may also be ascertained through the Status tool for machines, refinements and implementations).

Currently the Toolkit provides the following tools for supporting software development:

  1. A specification, design and code configuration management system, including integrity and dependency management and source file editing facilities.
  2. A set of software specification and design analysis tools, which includes syntax checkers, type checkers and a specification animator.
  3. A set of verification tools, which includes a proof-obligation generator and fully-automatic , semi-automatic  and fully-interactive provers, together with a proof printer for displaying proof obligations/proofs.
  4. A set of coding tools, which includes a translator, linker, rapid prototyping facilities and a reusable specification/code module library.
  5. Facilities to supplement the reusable library.
  6. A set of generators providing facilities to generate: base object AMN specification/implementations (the latter implemented on the reusable library) from simple declarative descriptions of structured data, enumerators providing i/o facilities for enumerated sets, and interfaces (either specification/implementations - again built on the reusable library, or alternatively on the X/Motif library ) to provide a run time environment.
  7. A documentation tool for automatically producing fully cross-referenced and indexed type-set documents from source files, together with facilities to display on screen or send to a printer.
  8. A re-making tool for automatically re-checking and re-generating specifications, designs, code and documentation after modifications to source files.
  9. A hypertext tool providing, in hypertext form, the facility to navigate through an entire development; each hypertext construct is automatically built from its Abstract Machine  or code file, allowing constructs external to the development (for example, informal requirements) to be hypertext-linked to the formal development.
  10. An overview tool providing, in picture form, the facility to navigate through an entire development via a Motif push- button interface; it provides views of both specification construction and design, enabling the user to see a complete picture of the development, or to zoom in on a particular aspect of it.
Before using the toolkit, the mandatory environment variable BKIT must be correctly set (see the `B-Toolkit Installation Guide').

Options may be set to customise the toolkit: settings for Remake, Construct Display, Editors/Viewers/Shell, Documents, Translators/Compilers, Provers, Interface, Bell , Optional Utilites and Teamlib may be set together with the facliity to save and restore global settings.

The B-Toolkit is invoked by issuing the command BToolkit (this script residing in the $BKIT directory) from a suitable development directory - any directory in which you have read-write permission.

Development Environment

If the toolkit is invoked where there is no existing development environment (which will be the case when it is invoked for the first time in a directory), the user is asked whether a new environment should be created. If the reply is `no' then the Toolkit is exited; if the reply is `yes' a new development environment, consisting of a set of development directories and configuration files, is created. The following directories are created if they do not already exist:

The Motif Interface

Motif Interface See figure