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 B 3.7
- ComenC translator