B4free is a set of tools for the development of B models.
B4Free, is the single-user version of Atelier
B with the capability of generating code C with CommenC translator. Components are limited to 4000 proof
obligations. B4Free is mainly aimed at the university academic environment but
also anyone wishing to become initiated into B tools.
The principal tool
(bbatch) manages B projects.
The Logic Solver (krt)
is a compiler-interpreter for the Theory Language.
All these tools are used in batch mode.
A graphic interface, based on B4free and developed by Jean-Raymond
Abrial and Dominique Cansell, is available on
Click'n'Prove page.
An online tutorial is available here, presenting the tool with an example. This tutorial was initially designed by Dominique Cansell.
A distribution of B4free and Click'n'Prove on one CD-ROM to be run, along with a Linux system inside Microsoft Windows, is available. : more information...
