Biomedical Engineering Reference
In-Depth Information
Ta b l e 7 . 3
Event-B to Java & C# translation syntax
Event-B
'Java' & 'C#'
Comment
n..m
short
Integer type
x
∈
Y
Y x;
Scalar declaration
x
∈
tl_int16
short x; (Java) &
ushort x; (C#)
'Java' & 'C#' contexts
x
∈
n..m
→
Y
Y [ ]x
=
new Y[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
≤
if(x
<
=
x
y
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
public long fun(long
arg
1,
long
arg
2)
{
//TODO: Add your Code
return;
}
Function definition
Search WWH ::
Custom Search