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

Table 1. Data constraints as contracts

Component
[ ϕ ]? m [ π ]
assume ϕ
guarantee π
[ ϕ ]! n [ π ]
guarantee ϕ
assume π

and hence, like the postcondition in input labels, must be a transition predicate
over the provided and the internal state variables.

Example 3. An example of an input label is the Σ Leg -label

maxStep ]? swing ( a )[ currStep = a steps = steps +1]

[ a ≤ ∧

where maxStep and currStep are provided state variables, and steps is an in-
ternal state variable of component Leg . The primed expression currStep in the
postcondition indicates that we refer to the value of currStep in the poststate.
For component LegC , the expression

gone , maxStep )] ! swing ( a )[ currStep ≤

[ a =min( distance − a ]

is a valid Σ LegC -label. This label expresses that the output swing ( a )happensif
the precondition ϕ gone , maxStep )] is satisfied. Note that

ϕ involves all three kinds of state variables: the provided state variable distance ,
the required state variable maxStep and the internal state variable gone .The
postcondition π

≡ [ a =min( distance −

[ currStep ≤

≡ a ] involves (beside the parameter a )therequired

state variable currStep .

Definition 2 (MIOD). A modal I/O-transition system with data constraints

S =( states S , start S ,Σ S ,Δ may

,Δ must
S

)

S

consists of a set of states states S , the initial state start S ∈ states S ,anI/O-

signature Σ S , a may-transition relation Δ may

⊆ states S ×L ( Σ S ) × states S ,and

S

Δ ma S . The class of all MIODs is denoted by

a must-transition relation Δ must
S

⊆

MIOD

. The set of the (syntactically) reachable states of a MIOD S is defined by

( S )= n =0 R n ( S ) where R R 0 ( S )= {

start S }

R n +1 ( S )= { s |∃

( s, , s )

∈

and

Δ may
S

such that s

∈R n ( S ) }

.

Example 4. The MIOD S Leg specifying the behavior of the Leg component is
shown in Fig. 1. Must-transitions are drawn with solid arrows and may-transitions
with dashed arrows. Preconditions are written above or to the left of operations;