Biomedical Engineering Reference
In-Depth Information
/
∗
In the
'
C
++'
Language
∗
/
BOOL SetFun
()
{
...
set < int > tset
2
;
set
_
union(A.begin(), A.end(), B.begin(), B.end(),
inserter(tset
2
, tset
2
.begin()))
;
if ((includes(C.begin(), C.end(), tset2.begin(),
tset
2
.end())))
{
.
EVENT SetFun
...
WHEN
...
grd3
/
∗
∗
/
private boolean SetFun
()
{
...
if (isSubset(unionSet(A, B), C))
{
.
In the Java language
:
A
∪
B
⊆
C
.
/
∗
In the C
#
language
∗
/
private boolean SetFun
()
{
...
A.UnionWith(B)
;
if (A.IsSubsetOf (C))
{
.
•
To Process Event's Action
The next sub-stage of an event translation presents the action translation. In
E
VENT
-B, all action predicates of an event are considered as in the form of con-
current execution. The set of action predicates are post-conditions in the Event-B
events, which state that all action predicates only valid when all pre-conditions or
guards are satisfied [
1
,
2
]. Event-B modelling approach supports that any state
variable is not allowed to be modified by different action expressions, means
Event-B ensures that any state variable used as an action assignee is not modified
by any prior post conditions or action predicate. In the code translation process,
all action predicates are generated into equivalent programming expression. In a
programming language, all action expressions are executed in a sequential order
of what they have defined in a formal specification. But all action expressions are
executed only when all
if
conditions become
true
. Event-B supports three kinds
of assignment operators
becomes equal to
(
:=
:∈
),
becomes in
(
) and
becomes
such that
(
) are used basi-
cally in an abstract model, and through the refinement process, it is represented
in a concrete form as
becomes equal to
(
:|
), where
becomes in
(
:∈
) and
become such that
(
:|
:=
). The translation tools only supports
becomes equal to
(
:=
). If a concrete model uses any
becomes such that
(
:|
) and
becomes in
(
) assignment operators, then the translation tool does not gener-
ate action predicates into programming expressions and move to the next action
predicate to continue processing. A similar way of parsing is applied on Event-B
action statement like a guard statement. The translation tool translates all Event-B
actions into an equivalent target programming language source code.
:∈
Search WWH ::
Custom Search