EB2ALL: An Automatic Code Generation Tool - Using Event-B for Critical Device Software Systems - page 120

A set of context files is used as an input to declare all kinds of data-types in form
of global constants on top of the source code file. All elements of the context files
are declared as global. Context element type information is derived from the type-
defining AXIOM statement within the context, which may express as integer ranges,
specially supported bit-map types or arrays of these defined by mapping functions.

Process Machine Files

Machine file contains dynamic behaviour of a system, which is denoted by gener-
ally variables , arrays , functions and events . All these components of a machine file
model a system. In the following section, we present automatic transformation of a
machine model into any programming language (C, C++, Java and C#).

Mapping Event-B Variable Types to Programming Language

A machine file contains functions , arrays and variables for representing a system
state. All these elements are declared as global. Global element's type information is
derived from the type-defining INVARIANT statements within the machine, which
may be expressed as integer ranges, function structure, or arrays. Event-B to target
language code generator generates target language function definitions correspond-
ing to the invariants. Event-B functions are generated explicitly into the target lan-
guage code and function definitions are placed in the corresponding source file. The
translation tool translates all those into target programming language code accord-
ing to the same rules, which are defined in the last section for defining a constant
type. Static and dynamic type definitions have only difference between context and
machine modules data types. For instance, constants and variables have the same
definition using primitive data types but C, C++ and C# language constants use
const keyword and Java uses static final keyword with a constant data type declara-
tion, and variables are defined in all languages without using const and static final
keywords.
More than one invariants or axioms may be defined in a single invariant or axiom
using and ( ) logical operator. This translation tool automatically parses an invari-

ant or axioms at the time of constant or variable data type declaration during the
translation process.

∧

C , and C ++
int var ;

Event - B
var

C #
short var ∈ tl _ int 16 ;

Java
short var ;