Information Technology Reference
In-Depth Information
Note that
T
is defined as a partial function, i.e., it produces a new model only for some
acceptable input models
s
and configurations
c
, i.e., when
(
s, c
)
∈
dom(
T
)
.
Definition 2.
A refinement pattern is a transformation rule
P
:
S
S
that
constructs a model refinement for any acceptable input model and configuration:
×
C
→
∀
s, c.
(
s, c
)
∈
dom(
P
)
⇒
s
P
(
s, c
)
where
denotes a refinement relation.
In this paper we rely on the Event-B proof theory when demonstrating that a transfor-
mation rule is indeed a refinement pattern.
3.2
The Language of Transformations
We propose a special language to construct transformation rules. The proposed lan-
guage contains basic transformation rules as well as the constructs allowing to com-
pose complex rules from simpler ones. For instance, a refinement pattern is usually
composed from several basic transformation rules. These rules themselves might not
be refinement patterns. However, by attaching to them additional proof obligations, we
can verify that their composition becomes a refinement pattern.
The structure of the basic rules reflects the way a transformation rule or a refinement
pattern is applied. First, rule applicability for a given input model and configuration
parameters is checked. The applicability condition to be checked can contain both syn-
tactic and semantic constraints on input models and configurations. Mathematically, for
a transformation rule
T
, its applicability condition corresponds to
dom(
T
)
. Then, the
input model
s
for the given configuration
c
is syntactically transformed into the output
model calculated as function application
T
(
s, c
)
. Finally, in case of a refinement pattern,
the result
T
(
s, c
)
should be demonstrated to be a refinement of the input model
s
, i.e.,
s
T
(
s, c
)
. The last expression, using the proof theory of Event B, can be simplified
to specific proof obligations on model elements to be verified.
A basic rule has the following general form:
rule
name
(
c
)
context
Q
(
c, s
)
effect
E
(
c, s
)
proof obligation
PO
1
(
c, s
)
...
proof obligation
PO
n
(
c, s
)
Here
name
and
c
are correspondingly the rule name and the list of its parameters.
The predicate
Q
(
c, s
)
defines the rule application context (applicability conditions),
where
s
is the model being transformed. The effect function
E
(
c, s
)
computes a new
model from a current model
s
and parameters
c
. The proof obligation part contains a
list of theorems to be proved to establish that the rule is a (part of) refinement pattern
and not just a transformation rule. From now on, we write
context
(
r
)
,
effect
(
r
)
and
proof obligations
(
r
)
to refer to the context, effect computation function, and collection
of proof obligations of a rule
r
.
