B4Free Presentation

What is B4Free ?

B4Free allows for Method B to be used operationally and offers numerous functionalities to manage projects in B language within a coherent environment:

Syntactic verification of models, automatic generation of theorems to be demonstrated, automatic translation of low level B models to C and Ada languages,
Proof support to automatically demonstrate the theorems,
Support in development: automatic management of dependencies between B components, reusable libraries, generation of documentation and metrics,
Graphic representation of projects, hypertext browser to surf within a project, project status and statistics display, automatic generation of a dictionary with project terms, project archiving.

History of the Versions

B4Free Version 3.2

based on Atelier B3.7
ComenC translator