Biomedical Engineering Reference
In-Depth Information
/
∗
In the
'
C
'
Language
∗
/
BOOL Sum
()
{
...
Ans
EVENT Sum
...
WHEN
...
THEN
act1
:
Ans
:=
a
+
10
−
6
∗
8
.
=
a
+
10
−
6
∗
8
;
.
/
∗
In the Java language
∗
/
private boolean Sum
()
{
...
Ans
=
a
+
−
∗
;
10
6
8
.
An action translation supports assignments to scalar variables, override state-
ments acting on array-type variables, arithmetic complex expressions and set op-
erations. The Event-B supports a special form of the action predicates, which
shows that a state variable can be used in the right side of the assignment opera-
tor (
). To handle such kinds of action predicates, the translation tool automati-
cally modifies the action predicates through a re-write phase and store the value
in an intermediate local variable, and finally translate into programming language
expression with an assignee in the action expression.
:=
/
∗
In the
'
C
'
Language
∗
/
BOOL Sum
()
{
...
OvrVar
[
3
]=
67
;
OvrVar
[
4
]=
88
;
EVENT Sum
...
WHEN
...
THEN
act1
OvrVar
[
t
]=
56
;
Arr
[
i
]=
5
;
.
:
OvrVar
:=
OvrVar
−
/
∗
In the Java language
∗
/
{
3
→
67
,
4
→
88
,t
→
56
}
private boolean Sum
()
{
act1
:
Arr(i)
:=
5
...
OvrVar
.
;
OvrVar
[
4
]=
88
;
OvrVar
[
t
]=
56
;
Arr
[
i
]=
5
;
.
[
3
]=
67
After insertion of all kinds of action predicates through the translation process
into a generated code event function, adds an extra statement returning a boolean
true
, which express run-time traceability and states that an event function is trig-
gered successfully. After insertion of returning boolean statement, inserts all curly
braces (}) according to the total number of guards except those guards, who repre-
sents local variable data types. Finally, a returning boolean
false
statement again
inserts before closing the final braces of an event function. The main objective
of this
false
boolean returning statement at a time of execution is that, when this
Search WWH ::
Custom Search