Biomedical Engineering Reference
In-Depth Information
Ta b l e 7 . 5
Equivalence between Event-B and programming language
Event-B types
Target language types
Enumerated sets
Enumerated types
Basic integer sets
Predefined integer types
Event-B array types
Target programming language array type
Function
Target programming language function structure
Sets theory
Set theory implementation using advanced library
function in target language (not in 'C')
CandC
++
enum ESet
{
On, Off
};
Event
-
B
partition(ESet,
{
On
}
,
{
Off
}
)
Java and C
#
public enum ESet
{
On, Off
};
•
The Numeric Types
The links between Event-B and target programming languages for integer values
have been considered as crucial for the efficiency of a generated code and for the
correctness of the translation process. So, the solution is provided in the second
phase by introducing target programming language context, and it is able to in-
terface very tightly between Event-B types and a target programming language
type. The Event-B numeric types (
) are either all mapped to the pre-
defined context files (see second phase of the translation process) or defined the
maximum integer range according to a programming language. For translating
constant data type in C, C++ and C# programming languages use
const
keyword,
while Java uses
static final
keyword for defining a constant.
N
,
N
1
and
Z
C
,
and C
++
const long int Lnum
;
Event
-
B
Lnum
∈ N
C
#
const long Lnum
;
Java
static final long Lnum
;
•
The Array Type
The links between Event-B arrays and target programming language arrays are
not straightforward. In Event-B, an array corresponds to a total function whereas
in the target programming language, an array corresponds to a contiguous zone
of memory (coded as the beginning address of the array and its size). However,
it is easy to do a semantical correspondence between an array element
arr(i)
in
Event-B and a value at the location
arr[i]
in target programming languages (see
Tables
7.2
,
7.3
).
Search WWH ::
Custom Search