Biomedical Engineering Reference
In-Depth Information
Ta b l e 7 . 1
Integer bounded data type declaration in different context files
Event-B type
Formal range
C & C++ type
Java type
C# type
2
15
..
2
15
tl
_
int
16
−
−
1
int
short
short
0
..
2
16
tl
_
uint
16
−
1
unsigned int
-
ushort
2
31
..
2
31
tl
_
int
32
−
−
1
long int
int
int
0
..
2
32
tl
_
uint
32
−
1
unsigned long int
-
uint
2
63
..
2
63
tl
_
int
64
−
−
1
-
long
long
0
..
2
64
tl
_
uint
64
−
1
-
-
ulong
•
enumerated types (including the boolean type)
•
bounded integer type (from MININT to MAXINT)
•
arrays on finite index intervals where the type of elements is a concrete type (in
set theory, they are similar for total functions)
Refinement Using a New Context File
A new context file consists of a new data type definition equivalent to the primary
data type (see Table
7.1
). This new context file helps to model a system more de-
terministic through transforming abstract data types into concrete data types. Here,
we consider the Event-B data types as the abstract data types, and the programming
language data type as the concrete data types. A refinement technique is used to in-
troduce a set of new concrete data types in the formal model. In this new refinement
process, a developer can replace all the Event-B abstract data types of the contexts
and the last concrete machine models, corresponding to the concrete data types ac-
cording to the selected target programming language. The following figure presents
an example for transforming an abstract data type into concrete data type.
var
1
∈
tl
_
int
16
var
1
∈
tl
_
int
32
var
1
∈
tl
_
int
64
var
1
∈ Z
var
2
∈
tl
_
uint
16
var
2
∈
tl
_
uint
32
var
2
∈
tl
_
uint
64
var
2
∈ N
A developer can skip this refinement level. In case of skipping of this refinement
level in the translation process, the translator generates default maximum bounded
integer primitive data type for all the variables and constants. New redefined deter-
ministic ranges using refinement generates a lot of proof obligations.
Search WWH ::
Custom Search