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

postconditions are written below or to the right of operations. Pre- and post-
conditions of the form [ true ] are omitted.
In the initial state 0, Leg can receive init () which has the effect of initializing
the internal state variable steps with 0. In state 1 the leg is able to receive lift (),
and then swing ( a ); in the latter case, the leg component assumes that the value
of the parameter a does not exceed the limit maxStep more than ten percent;
the maximal step size maxStep is a provided state variable, hence visible for the
connected leg controller. The guarantee of the leg component is then, that the
current step size is a and that the number of steps is increased by one. Next,
in state 3, the leg is put on the ground when the operation drop () is received,
and then, on reception of the operation call retract (), the leg is pulling the body
forward. Finally, an update message is sent to inform the leg controller how far
the leg has been moved forward.

? init () [ steps =0]

? lift ()

0 1 2

[ a ≤ maxStep + maxStep/ 10]

? swing ( a )

[ a = currStep ]

[ currStep = a
∧ steps = steps +1]

! update ( a )

5 4 3

? drop ()

? retract ()

Fig. 1. Specification S Leg of the Leg component

3 Refinement of MIODs

The basic idea of modal refinement is that any required ( must ) transition in
the abstract specification must also be present in the concrete specification.
Conversely, any allowed ( may ) transition in the concrete specification must be
allowed by the abstract specification. Modal refinement has the following conse-
quences: A concrete specification may omit allowed transitions, but is required to
keep all must-transitions. Moreover, it is not allowed to perform more transitions
than the abstract specification admits.
Concerning the impact of data constraints, let us first consider required (i.e.
must ) transitions of an abstract MIOD, say T , see Def. 3(1). Obviously, any
such transition with a precondition ϕ T must also be executable in a refinement
S , whenever ϕ T is valid. Hence there should be a corresponding must-transition
in S whose precondition ϕ S does not require more than ϕ T does. This condition is
independent of the kind of the labels. Concerning postconditions the situation is
different because postconditions are not related to the executability of transitions