B Compiler


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 !

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.


  1. ↑ The B language Reference Manual [1]