A Modal Interface Theory with Data Constraints - Formal Methods: Foundations and Applications - page 89

[ true ]? swing ( a )[ currStep ≤ a ]

t L

t L

T Leg

[ a ≤ maxStep ]? swing ( a )[ currStep = a ]

S Leg

[ a ≤ maxStep + maxStep/ 10]

? swing ( a )

[ currStep = a ∧ steps = steps +1]

s L s L

Fig. 2. Refinement S Leg of an abstract specification T Leg

Example 5. Fig. 2 shows excerpts of two MIODs specifying the component Leg ,
an abstract specification T Leg and the more concrete specification S Leg ,seealso
Fig. 1, which refines T Leg , i.e. S Leg ≤ m T Leg . The abstract specification T Leg
expresses that under the precondition [ a maxStep ] a call to the operation

swing ( a ) must be accepted in any implementation such that in the state after
execution of the operation, the postcondition [ currStep = a ] is satisfied. The
proper may-transition of T Leg says that also such implementations are allowed
which accept the operation call swing ( a ) in states not satisfying [ a

≤

≤ maxStep ],

and then the postcondition [ currStep ≤ a ] must be satisfied in the next state.

In the refinement S Leg there is only a must-transition. The refinement relation
holds since, as required by condition 1 in Def. 3, for the must-transition in T Leg
there is a corresponding must-transition in S Leg such that the precondition is
weakened (by allowing also values of the parameter a exceeding the maximal step
size at most by ten percent) and, according to 1(a) in Def. 3, the postcondition
is strengthened by requiring additionally [ steps = steps + 1]. Conversely, for
the direction from S Leg to T Leg , condition 2 in Def. 3 requires that the must-
transition (which is also a may-transition) in S Leg is allowed by the abstract
specification T Leg . This is indeed the case because for the transition in S Leg
there is a corresponding may-transition in T Leg such that the precondition is

weakened in T Leg and, according to 2(a) in Def. 3, the postcondition in S Leg

is

stronger than the corresponding postcondition in T Leg .

4 Composition and Compatibility of MIODs

MIODs can be composed to specify the behavior of concurrent systems of inter-
acting components with data constraints. The composition operator extends the
synchronous composition of modal I/O-transition systems [9]. Like for MIOs, we
need some syntactic restrictions under which two MIODs are composable. First,
we require that overlapping of operations only happens on complementary types
and that the same holds for state variables.