Information Technology Reference
In-Depth Information
p ( c )= basic ( c )
primitive rule
| p ; q
sequential composition
| pq
parallel composition
| if Q ( c, s ) then p end
conditional rule
| conf i : Q ( i, c, s ) do p ( i ∪ c ) end
parameterised rule
| par i : Q ( i, c, s ) do p ( i ∪ c ) end
generalised parallel composition
Fig. 1. The language of transformation rules
3.3
Examples
In this section we present a couple of simple examples of refinement patterns con-
structed using the proposed language.
Example 1 (New Variable). A refinement step adding a new variable can be accom-
plished in three steps. First, the new variable is added to the list of model variables.
Second, the typing invariant is added to the model. Finally, an initialisation action is
provided for the variable. The following refinement pattern adds a new variable de-
clared to be a natural number and initalised with zero:
conf v : ¬ ( v ∈ s.var ) do
newvar ( {v} );
( newinv ( { v ∈ N },s ) newact ( init , {v | := | ”0” } ))
end
The only pattern parameter (apart from the implicit input s ) is some fresh name for the
new model variable.
A pattern application example is given below. The left-hand side model is an input
model and the righ-hand side is the refined version constructed by the pattern. The
example assumes that variable name q is chosen for parameter v .
MACHINE m 0
VARIABLES x
INVARIANT x
MACHINE m 1
VARIABLES x, q
INVARIANT x
Z
INITIALISATION x := 0
EVENTS
count = BEGIN x := x +1 END
N
INITIALISATION x := 0
Z
q
q := 0
EVENTS
count = BEGIN x := x +1 END
A more general (and also useful) pattern version could accept a typing predicate and an
initialisation action as additional pattern parameters.
Example 2 (Action Split). In Event B, an abstract event may be refined into a choice
between two or more concrete events, each of which must be a refinement of the abstract
event. A simple case of such refinement is implemented by the refinement pattern below.
The pattern creates a copy of an abstract event and adds a new guard and its negation to
the original and new events. The guard expression is supplied as a pattern parameter.
Search WWH ::




Custom Search