Biomedical Engineering Reference
In-Depth Information
/
∗
In the
'
C
'
Language
∗
/
BOOL Sum
()
{
long int a
;
EVENT Sum
ANY
a
WHEN
grd1
:
a
∈ N
.
.
/
∗
In the Java language
∗
/
private boolean Sum
()
{
long a
;
.
•
To Process Event's Guard
In the Event-B, guard handling is very ambiguous due to contain several kinds of
modelling notations, such that local variable type definition, conditions and use
of different kinds of logical operators (
). Therefore, for handling
so many complex situations, we have designed a recursive algorithm for parsing a
complex guard and to separate different kinds of predicates in the form of formal
notations for generating a programming language code using guards. Thus, each
guard must be automatically analysed to resolve this ambiguity from the context
information. In a formal model, the guards are known as pre-conditions and ac-
tion predicates are known as post-conditions. In an event, all pre-conditions must
be true for executing the post-conditions or action predicates. For translating an
event of a formal model into a programming language, we translate it into corre-
sponding target language function (C, C++, Java and C#).
Pre-conditions of a guard are translated into equivalent
if
condition statement.
A group of guards is translated in the form of
nested-if
conditions, and are placed
into an event function as a set of nested conditional statements, using directly
translated conditional and local variables declared within nested scope ranges.
A suitable comment is also inserted with each guard condition to understand the
different elements of the guards like local variables and pre-conditions.
∧
,
∨
,
¬
,
⇒
,
⇔
EVENT Sum
...
WHEN
...
grd3
:
a<n
grd4
:
a>m
.
/
∗
∗
/
/
∗
∗
/
In the
'
C
'
Language
In the Java language
BOOL Sum
()
{
...
if (a < n)
{
if (b > m)
{
.
private boolean Sum
()
{
...
if (a < n)
{
if (b > m)
{
.
Search WWH ::
Custom Search