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

C , and C ++
const long int ARR [ 11 ];

C #
const Event - B

ARR

[] long = new long [ 11 ];

∈ 1 .. 10 → N

Java
static final [] long = new long [ 11 ];

• The Function Type

The links between Event-B function and target programming language function is
also very ambiguous. The Event-B functions are generated explicitly into a target
language code, and function definitions are placed in the corresponding source
file. The translation tools only supports total function of Event-B into equiva-
lent corresponding target programming language function. However, it is an easy
way to do a semantical correspondence between function passing parameters in a
target programming language is equivalent to the elements of left side of the to-
tal functions symbol (

) and output of a target programming language function
corresponds to the right-hand side of the total functions symbol (

→

) in Event-B.
So, this step of function translation generates a function structure into a target
programming language (see Tables 7.2 , 7.3 ).

→

C , and C ++
unsigned long int (unsigned long int arg 1 ,
unsigned long int arg 2 )
{

//TODO : Add your Code

return ;

}

Event - B
fun ∈ N × N → N

Java
public long (long arg 1 , long arg 2 )
{

//TODO : Add your Code

return ;

}

• The Set Type

The translation tool is a set of plug-ins, in which C++, Java and C# languages
plug-ins can support Sets formal notation for translation. The Event-B sets type
is translated into a programming language using the standard template library
(STL) in C++, advanced Java class utilities in Java and Generic Collection of
.NET Framework in C#. We have developed some functions with the help of
existing library functions in C++, Java and C#, which are equivalent to Event-B