The BToolkit, a toolkit supporting software development with the B-method.
C HTML GAP Shell Isabelle C++ Other
Failed to load latest commit information.
B2DOORS Added B to DOORS presentation. FME99. Jun 16, 2014
BDEMO demo files need not be executable May 8, 2014
BPALETTE extra newlines removed May 29, 2014
C For this to work on MAC OS, file paths longer than 250 characters are… Jan 29, 2015
LIB BSD-2 changed to Boost Software License 1 Jan 12, 2015
MOTIF Increased robustness, added stronger guards Feb 26, 2015
SCRIPTS non-binaries should not be executable May 8, 2014
SRC text files should not be executable May 8, 2014
UTIL Use applescript bundle Feb 6, 2015
.gitignore Use applescript bundle Feb 6, 2015
INSTALL Added Yosemite installation instructions Feb 6, 2015
LICENSE License Oct 9, 2013 Update Jan 12, 2015


The BToolkit is a toolkit supporting software development with the B-method.

The B-Method was initially devised by Jean-Raymond Abrial during his time at the Programming Research Group at the University of Oxford. Then the B tools were developed at BP Research. BP assigned the rights for these tools to B-Core (UK) Ltd. The B-Toolkit was developed at B-Core by Ib Sorensen and David Neilson from 1992.

The source code to the B-Toolkit has been posted in memory of Ib Sorensen. Ib Sorensen - In memoriam

B-Core no longer supports or maintains the B-Toolkit.

About B

B is a generic term given to a method of software development, the B-Method, its process and notation and to its supporting toolset, the B-Toolkit.

B is a sound, mathematically-based technology for application within a practical Software Process.

The B-Method is designed to provide a notation and a method for requirements modeling, software interface specification, software design, implementation and maintenance, thus supporting the major phases of a software process. Incremental construction of layered software as well as its incremental verification and validation are the guiding principles of the B-Method.

The B-Toolkit supports the B-method over the entire software process and comprises a large suite of tools which can run automatically or interactively. The tool supports the incremental construction of the software. The validation processes are supported by static analysis, by dynamic analysis using simulation, as well as proof of correctness using an integrated theorem prover (the B-ToolProvers).


The tool itself is licensed under the BSD 2-clause license.

The source code that is used as the implementation for library machines and may form part of the source code that is output from the tool, is licensed under the Boost Software License.

Please feel free to get in touch if you have any questions or even to say what you might use the BToolkit source for.

See my homepage for details.