Information Technology Reference
In-Depth Information
The consistency requirements for the sequential composition, conditional and parame-
terised rules are quite standard. Two rules can be applied in parallel if they are work-
ing on disjoint scopes. For instance, a rule transforming an event (e.g., adding a new
guard) cannot be composed with another rule transforming the same event. A similar
requirement is formulated for the loop rule, since it is realised as generalised parallel
composition.
The rule scopes are calculated by using the predefined function
,whichre-
turns a pair of lists, containing the model elements that the rule updates or depends on.
Intersection of rule scopes is computed as an intersection of the elements updated by
the transformations and the pair-wise intersection of elements updated by one rule and
depended on by another:
scope
inter
((
r
1
,w
1
)
,
(
r
2
,w
2
)) = (
w
1
∩
w
2
)
∪
(
r
1
∩
w
2
)
∪
(
r
2
∩
w
1
)
4.2 Effect of Pattern Application
Once the rule applicability conditions are met, an output model can be syntactically
constructed in a compositional way. For a basic rule, the effect function is directly ap-
plied to transform an input model. For more complex rules, a new model is constructed
according to an inductive definition of the function
eff
given below.
eff
(
basic
)(
c, s
)
=
effect
(
basic
)(
c, s
)
eff
(
p
;
q
)(
c, s
)
=
eff
(
q
)(
c,
eff
(
p
)(
c, s
))
eff
(
pq
)(
c, s
)
=
eff
(
q
)(
c,
eff
(
p
)(
c, s
))
,
or
=
eff
(
p
)(
c,
eff
(
q
)(
c, s
))
eff
(
if
G
(
c, s
)
then
p
end
)(
c, s
) =
eff
(
p
)(
c, s
)
,
if
G
(
c, s
)
=
s,
otherwise
eff
(
conf
i
:
Q
(
i, c, s
)
do
p
(
i
)
end
)(
c, s
)=
eff
(
p
(
i
))(
c, s
)
,
if
Q
(
i, c, s
)
=
s,
otherwise
eff
(
par
i
:
Q
(
i, c, s
)
do
p
(
i
)
end
)(
c, s
)=
eff
(
i ∈ Q
(
i, c, s
)
· p
(
i
)) (
c, s
)
,
if
∃ i, c, s · Q
(
i, c, s
)
=
s,
otherwise
As expected, the result of sequential composition of two rules is computed by applying
the second rule to the result of the first rule. For parallel composition, the result is
computed in the same manner but the order of the rules should not affect the overall
result. The resulting model of the loop construct is computed as generalised parallel
composition of an indexed family of transformation rules. The last three cases depend
on some additional application conditions (i.e.,
G
(
c, s
)
or
Q
(
i, c, s
)
). If these conditions
are not true, rule application leaves the input model unchanged.
The rule application procedure based on the presented definition can be easily auto-
mated. The only interesting detail is in providing input values for the rule parameters.
In our tool implementation for the Event-B method, briefly covered later, the user is
requested to provide the parameter values during rule instantiation, while appropriate
contextual hints and descriptions are provided by the tool.
4.3 Pattern Proof Obligations
To demonstrate that a rule is a refinement pattern, we have to discharge all the proof
obligations of individual basic rules occurring in the rule body. These proof obligations
