Biomedical Engineering Reference
In-Depth Information
Ta b l e 7 . 2
Event-B to C & C++ translation syntax
Event-B
'C' & 'C++' language
Comment
n..m
int
Integer type
x
Y
Y x;
Scalar declaration
x
tl_int16
int x;
'C' & 'C++' contexts
x
n..m
Y
Y x [m
+
1];
Array declaration
x
:∈
Y
/* No action */
Indeterminate init.
x :| Y
/* No action */
Indeterminate init.
x = y
if(x == y) {
Conditional
x = y
if(x! = y) {
Conditional
x < y
if(x < y) {
Conditional
x y
if(x < = y) {
Conditional
x > y
if(x > y) {
Conditional
x
y
if(x > =
y) {
Conditional
(x > y)
(x
z)
if ((x > y) && (x > =
z)) {
Conditional
(x > y)
(x
z)
if ((x > y)
(x > =
z)) {
Conditional
x
:=
y
+
z
x
=
y
+
z;
Arithmetic assignment
x
:=
y
z
x
=
y
z;
Arithmetic assignment
x
:=
y
z
x
=
y
z;
Arithmetic assignment
x
:=
y
÷
z
x
=
y / z;
Arithmetic assignment
x
:=
F(y)
x
=
F(y);
Function assignment
a
:=
F(x
y)
a
=
F(x, y);
Function assignment
x
:=
a(y)
x
=
a[y];
Array assignment
x
:=
y
x
=
y;
Scalar action
a
:=
a
{x
y}
a[x]
=
y;
Array action
a
:=
a
{x
y}
{i
j}
a[x]
=
y; a[i]
=
j;
Array action
X
Y
if(!X
Y){
Logical implication
X Y
if((!X Y) && (!Y X)){
Logical equivalence
¬ x < y
if(!(x < y)){
Logical not
x ∈ N
unsigned long int x
Natural numbers
x ∈ Z
signed long int x
Integer numbers
/* No action */
Quantifier
/* No action */
Quantifier
fun
∈ N × N → N
unsigned long int fun(
unsigned long int arg 1,
unsigned long int arg 2)
{
//TODO: Add your Code
return;
}
Function definition
Search WWH ::




Custom Search