B4free est un ensemble d'outils dédié au développement de modèles B.
B4Free, c’est aussi l’Atelier B en version
mono-utilisateur, capable de générer du code C grâce au traducteur CommenC. Les composants sont
limités à 4000 obligations de preuve. B4Free s’adresse majoritairement au
milieu académique universitaire mais aussi à quiconque désirant s’initier aux
outils B.
L'outil principal (le bbatch) contrôle les projets B
Le Logic Solver (krt) est un compilateur-interprète pour la langue de théorie.
Tout ces outils sont utilisés dans le mode bbatch.
Une interface graphique, basée sur B4Free et développée par Jean-Raymond Abrial et Dominique Cansell, est disponible sur la page
Click'n'Prove.
Un tutoriel en ligne est disponible ici, et présente l'outil en faisant appel à un exemple. Ce tutoriel a été au commencement conçu par Dominique Cansell.
Une version de B4free et de Click'n'Prove pour Linux sous Microsoft Windows est disponible sur CD-ROM. Pour
plus d'informations...
