Biomedical Engineering Reference
In-Depth Information
Ta b l e 7 . 6
Event B events
Before-after predicate
BA(e)(x, x
)
Event
e
P(x,x
)
BEGIN
x
:|
(P (x, x
))
END
Q(x, x
)
WHEN
G(x)
THEN
x
:|
(Q(x, x
))
END
G(x)
∧
R(x,x
,t))
ANY WHEN
t
WHERE
G(t, x)
THEN
x
∃
t
·
(G(t, x)
∧
(R(x, x
,t))
:|
END
Mapping Event-B Events to Programming Language
The translation tool provides a recursive process to generate a source code for each
event of the Event-B specification into a target programming language. The trans-
lation tool always checks for
null
event (i.e. guard of a false condition), never gen-
erates a source code for that event, and inserts suitable comment into the source
code for the traceability purpose. This automatic reduction is performed to avoid
generation of an unreachable
run-time
code.
•
To Process Event's Variable
In Event-B specification, there are two kinds of variables: global variables and lo-
cal variables. Global variables are derived directly from
VARIABLES
statements
of a concrete machine, and all these variables have global scope. Local variables
are derived from the
ANY
statement of the particular event, and these are entirely
local to the corresponding event function (see Table
7.6
). The type of this local
variable is declared into the event's guards. Once the guards of an event have
been classified, and that conferring local variable type information are used for
variable declaration in a function. Remaining guards are used to generate local
assignment and conditional statements in the guard section. Local variable type
information is derived in a similar fashion as the global variables from the guard
predicates instead of using INVARIANTS. A recursive process is used to find a
type of Event-B local variable corresponding to the programming language. Each
event of Event-B is generated in equivalent to the programming language func-
tion. After generation of a function header, all local variables, array declarations
are inserted at the beginning of the function, giving them scope across the whole
function body.
Search WWH ::
Custom Search