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

There are three kinds of labels concerning reception (?), sending (!) and internal
execution of an operation. In each case, labels are equipped with pre- and post-
conditions represented by state and transition predicates over particular sets of
state variables.
Input labels. Alabel[ ϕ ]? m [ π ] models that if a provided operation m is invoked
under the precondition ϕ then the postcondition π will hold after the execution of
m .Inthiscase ϕ expresses the assumption (of the specified component) that the
environment will only call m when the component's data state fulfills ϕ . Hence
ϕ must be a state predicate over the provided state variables of the component
(possibly containing the operation's formal parameters as logical variables). In
particular, no internal state variables are allowed in ϕ , since it must be possible
for the environment to check whether the precondition ϕ is actually valid upon
operation call. The postcondition π models the change of the component's data
state caused by the execution of the operation m and hence it is a transition pred-
icate over the provided and the internal state variables of the component (again
possibly containing the operation's formal parameters as logical variables). In
this case π expresses the guarantee (of the specified component) that after the
execution of m the postcondition π holds (if the assumption ϕ was met) 1 .The
assumptions and guarantees of a component concerning input labels are part of
the contract principle behind data constraints as shown in Table 1.
Output labels. Alabel[ ϕ ]! n [ π ] models that a component issues a call to a required
operation n under the precondition ϕ and with postcondition π .Here ϕ describes
the condition under which the operation call is performed by a component.
Since the component has access to its own, provided and internal, state variables
and can also query its required state variables, the condition ϕ can contain all
kinds of state variables (together with the operation's formal parameters as
logical variables). From the contract point of view the component guarantees
to issue the call to the operation n only if ϕ holds 2 . The postcondition π of
an output label formulates the expectations on the change of the data state
performed by the environment after the invoked operation has been executed.
Hence π must be a transition predicate over the required state variables which
expresses an assumption on the environment. The assumptions and guarantees of
a component concerning output labels accomplish the contract principle behind
data constraints as shown in Table 1.
Internal labels. Finally, a label [ ϕ ] i [ π ] stands for the execution of an internal
operation i .Inthiscase ϕ describes the condition under which the internal
operation is executed which, like the precondition in output labels, can again
depend on all kinds of state variables. The postcondition π models the change
of the component's data state caused by the execution of the internal operation i
1 The environment can in fact only see the observable consequences of the guarantee
π w.r.t. the provided state variables.
2 In fact, the environment can only see the observable consequences of the guarantee
ϕ w.r.t. the required state variables.