Biomedical Engineering Reference
In-Depth Information
) in a guard predicate is a func-
tion of two arguments, such that for any predicate connected with an equivalence
operator (
Equivalence
(
⇔
): The equivalence operator (
⇔
⇔
) is translated as follows:
/
∗
In the
'
C
'
Language
∗
/
BOOL Sum
()
{
...
if ((
!
(a < b)
||
(P
_
State
==
FA L S E ))
||
(
!
(P
_
State
==
FA L S E )
||
(a < b)))
{
.
EVENT Sum
...
WHEN
...
grd3
:
a<b
⇔
P
_
State
=
FA L S E
.
/
∗
In the Java language
∗
/
private boolean Sum
()
{
...
if ((
!
(a < b)
||
(P
_
State
==
FA L S E ))
||
(
!
(P
_
State
==
FA L S E )
||
(a < b)))
{
.
Arithmetical expressions, calling functions and set operations (see Tables
7.2
,
7.3
) are also supported by Event-B formal notations in the guards, which are
all translatable into any target programming language. Event-B expressions and
statements are code generated, such that the generated code behaves like it is
expected from the specification. A set of translation rules with a basic syntactic
architecture is defined in Table
7.2
and Table
7.3
. Translation tool follows the
similar set of rules for generating a source code. A special kind of ambiguity of
a functional-image relation is resolved during the translation process, which may
be used to model a data array or an external function. The meaning of functional-
image statements within a model is automatically resolved to an array if the map-
ping is a global variable, otherwise to call an uninterpreted function. A complete
set of guards of an event is translated into equivalent programming language code
in the form of pre-conditions in an event. During the code translation process,
a run-time exception function is generated if an undefined expression or an error
statement is occurred. This call of exception function terminates the code trans-
lation and reports that an undefined expression into a code generation log file.
The translation tool can support a very complex predicate, where more than
one predicate are defined in a single guard. The translation tool is able to automat-
ically parse the whole predicate into a set of predicates, separately for translation
purpose.
Set operations
: The set operators (
) in a guard predicate is a function
of two arguments, which uses some intermediate steps according to the C++,
Java and C# programming languages. The translation of set based expression is
translated as follows:
∪
,
∩
,
\
Search WWH ::
Custom Search