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