B-Compiler Project
From ClearSy Tools
Contents |
Introduction
The B Compiler is, together with the Proof obligation Generator and the Theorem Prover, one of the most important tool of Atelier B CASE tool. The B Compiler performs syntax analysis on B models, checks typing coherency as well as architecture and visibility rules of B models. Refer to [1] for more details.
The B Compiler is also a powerful library that can be linked to applications manipulating B models (model analyzer, code generator, documentation generator, etc.).
Hands On
Tutorial & examples
- Tutorial : how to make use of the B Compiler Library (under construction)
- Practice Examples : examples of use and expansion of B_COMPILER (under redesign)
Reference manuals
- B compiler general design 1.6 (French)
- B compiler B0 check phase specification 1.3 (French)
- B compiler semantic phase specification 1.9 (French
- B compiler Btree manager specification 1.7 (French)
Wiki manuals
Those copies of .pdf documentations are, at the moment, under construction. The implementation is not totally completed, and we need to translate all docs from french to english & resolve all syntaxic problems.
Every help & contributions are welcome !
- B compiler general design 1.6 (translation completed)
- B compiler B0 check phase specification 1.3 (translation completed)
- B compiler semantic phase specification 1.9 (translation pending)
- B compiler Btree manager specification 1.7 (translation pending)
Sourceforge site
The B Compiler is going open-source (GPL v3.0) and is hosted on sourceforge. Source code and executable files are released & uploaded since summer 2008.