A Multi-target Code Generator for High-Level B

Within high-level specification languages such as B, code is refined in many steps until a small "implementable" subset of the language is reached. Then, code generators are used, targeting programming languages such as C or Ada. We aim to diminish the number of refinement steps needed, by providing an improved code generator. Indeed, many high-level operations and data types, such as sets, can be dealt with in programming languages such as Java and C++. We present a code generator for B named B2Program with two distinct features. Firstly, it targets multiple (high-level) languages via a template-based approach to compilation. In addition to flexibility, this also enables one to safeguard against errors in the individual compilers and standard libraries, by generating multiple implementations of the same formal model. Secondly, it supports higher-level constructs compared to existing code generators. This enables new uses of formal models, as prototypes, demonstrators or simply as very high-level programming languages, by directly embedding formal models as components into software systems. In the article, we discuss the implementation of our code generator, evaluate it using B models taken from literature and compare its performance with simulation in ProB.