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
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
Before using the toolkit, the mandatory environment variable BKIT
must be correctly set (see the `B-Toolkit
A specification, design and code configuration management system, including
integrity and dependency management and
source file editing facilities.
A set of software specification and design analysis
tools, which includes syntax checkers, type checkers and a specification
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.
A set of coding tools, which includes a translator,
prototyping facilities and a reusable specification/code module
Facilities to supplement the reusable
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.
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.
A re-making tool for automatically re-checking
and re-generating specifications, designs, code and documentation after
modifications to source files.
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.
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.
Options may be set to customise the toolkit:
settings for Remake, Construct
, 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
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
for source files
for files committed to configuration
for the intermediate analysed form
for TypeChecker information
for the proof obligation files
for Hypertext files
for typeset document files
for the proof method files
for C-program files
for temporary files
The Motif Interface