Information Technology Reference
In-Depth Information
As an example, let us consider two primitive rules for the Event-B method. The first
transformation adds one or more new variables:
rule
newvar
(
vv
)
context
vv ∩ s.var
=
∅
effect
s.var ∪ vv | s.inv | s.evt
proof obligation
∀ v ∈ vv ·
(
∃ a · a ∈ s.
init
.action ∧ v ∈ a.var
)
The rule applicability condition requires that the new variables have fresh names for the
input model. The effect function simply adds the new variables to the model structure.
The rule also has a single proof obligation requiring that the variable(s) is assigned in
the initialisation action. Such an action would have to be added by some other basic
rule for the same refinement step.
Another example is the rule for adding new model invariant(s).
rule
newinv
(
ii
)
context
ii ⊆
PRED
∧∀i ∈ ii · FV
(
ii
)
⊆ s.var
effect
s.var | inv ∪ ii | evt
proof obligation
∀ e, v, v
· e ∈ s.evt ∧
Inv
(
v
)
∧ Guards
e
(
v
)
∧ BA
e
(
v, v
)
⇒ Inv
(
v
)
proof obligation
∃ v · lnv
(
v
)
Here
FV
(
x
)
is set of free variables in
x
,
Inv
stands for (
i∈s.inv∪ii
i
),
Guards
e
is de-
fined as (
g∈e.guards
g
)and
BA
e
is the before-after predicate. Both proof obligations
are taken directly from the Event-B semantics (i.e., the corresponding proof obligation
rules). The first obligation requires to show that the new invariant is preserved by all
model events, while the second one checks feasibility of such an addition by asking to
prove that the new invariant is not contradictory. This example illustrates how the un-
derlying Event B semantics is used to derive proof obligations for refinement patterns.
The table below lists the basic rules for the chosen subset of Event B. There are
two classes of rules - for adding new elements and for removing existing ones. All
the rules implicitly take an additional argument - the model being transformed. A
double-character parameter name means that a rule accepts a set of elements, e.g.,
newgrd
(
e, gg
)
adds all the guards from a given set
gg
to an event
e
.
rule
newvar
(
vv
)
rule
delvar
(
vv
)
rule
newinv
(
ii
)
rule
delinv
(
ii
)
rule
newevt
(
ee
)
rule
delevt
(
ee
)
rule
newgrd
(
e, gg
)
rule
delgrd
(
e, gg
)
rule
newact
(
e, aa
)
rule
delact
(
e, aa
)
rule
newactexp
(
e, a, p
)
To construct more complex transformations, we introduce a number of composition
operators into our language. They include the sequential,
p
;
q
, and parallel,
p
q
,com-
position constructs. In addition, there is the conditional rule construct,
if
c
then
p
end
,
as well as a construct allowing us to introduce additional rule parameters -
conf
i
:
Q
do
p
(
i
)
end
. Finally, to handle rule repetitions, generalised parallel com-
position is introduced in the form of a loop construct:
par
c
:
Q
do
p
(
c
)
end
.The
language summary is given in Figure 1.
