Code generation

The B method is primarily intended to produce code with a high level of confidence, at the end of a development cycle combining formalism and mathematical proof. The approach used is to avoid introducing errors during development through proof, rather than using tests to discover them towards the end of development.

The code produced is derived from the translation of implementations written in the B0 language, a subset of the B language and with a syntax close to any structured language. The translation phase then produces a target code with a form similar to that of the B0 model.

This so-called “1-to-1” translation makes it easy to check the generator’s output code against the B0 model.