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

but rather to the specification of admissible poststates after a transition has
fired. In this case, if the transition of T concerns input or internal labels, the
corresponding transition of the refinement S should lead to a postcondition π S
which guarantees the postcondition π T of T (expected, for instance, by a user
of a provided operation who relies on the postcondition given in the abstract
specification T , see 1(a) in Def. 3). However, if a transition of T concerns an
output label, then the postcondition π T expresses the expectation of T about
the next state of the environment. Then, a refinement S should not expect more
than the abstract specification does, i.e. π S should be at most weaker than π T ,
see 1(b) in Def. 3.
Let us now consider may-transitions of the concrete MIOD S , see Def. 3(2).
Obviously, any such transition with a precondition ϕ S must be allowed by the
abstract specification T , whenever ϕ S is valid. Hence, there should be a corre-
sponding may-transition in T whose precondition ϕ T is at most weaker than ϕ S
and this condition is again independent of the kind of the labels. As explained
above the situation is different when considering postconditions since they are
not related to the executability of transitions. Therefore, in this case, the kind of
the transitions (may or must) is irrelevant and hence the requirements 2(a)(b)
coincide with the requirements 1(a)(b) in Def. 3.
In summary, we can observe that the implication direction concerning precon-
ditions in a refinement depends on the kind of the transitions (may or must) while
the implication direction concerning postconditions in a refinement depends on
the kind of the labels (input, internal, or output).

Definition 3 (Modal Refinement of MIODs). Let S and T be two MIODs
with the same I/O-signature Σ =( V , O ) .Abinaryrelation R ⊆ states S × states T

is a modal refinement between the states of S and T iff for all ( s, t ) ∈ R

,if ( t, [ ϕ T ] op [ π T ] ,t ) Δ must

T

1. (from abstract to concrete) for all op ∈O ∈ ,then

there exist s ∈ states S and a transition ( s, [ ϕ S ] op [ π S ] ,s ) Δ must

S

∈ such that

( s ,t ) ∈ R , ϕ T ⇒ ϕ S , and the following holds:

∈O prov ∪O int

(a) if op then π T ⇐ π S ,

∈O req then

π S .
2. (from concrete to abstract) for all op ∈O ,if ( s, [ ϕ S ] op [ π S ] ,s )

(b) if op π T ⇒

Δ may
S

∈ ,then

Δ may
T

there exist t ∈ states T and a transition ( t, [ ϕ T ] op [ π T ] ,t )

∈ such that

( s ,t )

∈ R , ϕ T ⇐ ϕ S , and the following holds:

∈O prov ∪O int then (a) if op π T ⇐ π S ,

(b) if op ∈O req then

π T ⇒ π S .

A state s

≤ m t ,iffthereexistsa
modal refinement between the states of S and T containing ( s, t ) . S is a modal
refinement of T , written S ≤ m T ,iffstart S ≤ m start T .

∈

states S refines a state t

∈

states T , written s

In the following, we will illustrate the concepts of refinement and, later on, com-
patibility by means of our running example. We will focus here on the treatment
of data constraints by considering small excerpts of corresponding MIODs.