Next: Parameterised Contracts as Generalisation
Up: Parametric Contracts
Previous: Parametric Contracts
Contents
Index
Before defining contracts
for components, we briefly review B. Meyer's design-by-contract principle from
an abstract point of view. According to [, p. 342], a contract
between the client and the supplier consists of two obligations:
- The client has to satisfy the precondition of the supplier.
- The supplier has to fulfil its postcondition, if the
precondition was met be the client.
Each of the above obligations can be seen as the benefit for the other
party. (The client can count on the postcondition if the precondition
was fulfilled, while the supplier can count on the
precondition). Putting it in one sentence:
If the client fulfils the
precondition of the supplier, the supplier will fulfil its
postcondition.
The used component plays the role of a supplier. But to formulate contracts
for components, we also have to identify the pre- and postconditions and the
user of a component. But what is to be considered a precondition,
postcondition and user depends whether the component is used at run-time or
configuration-time. Let's first consider the component's use at run-time.
Using a component at run-time is calling its services. Hence, the user of a
component
is the set of all components connected to
's provides-interface(s).
The precondition for that kind of use is the precondition of the service,
likewise the postcondition is the postcondition of the service. Actually, that
shows that this kind of use of a component is nothing different as using a
method. Therefore, the author considers this case as the use of a
component service, but not as the use of a component.
Likewise, the contract to be fulfilled here from client and supplier is a
method contract as described by B. Meyer already in 1992.
This is not the contract for using the component!
The other case of component usage (usage at composition-time) is actually the
relevant case when talking about the contractual use of components. This is
the important case when architecting systems out of components or deploying
components within existing systems for reconfigurations. Again, in this case a
component
is acting as a supplier and the environment as a client. The
component
offers services to the environment (i.e., the components
connected to
's provides-interface(s)). According to the above discussion
of contracts, these offered services are the postcondition of the component,
i.e., what the client can expect from a working component. Also
according to B. Meyer's above mentioned description of contracts, the precondition is what the component
expects from its environment (actually all
components connected to
's requires-interface(s)) to be provided by the
environment, in order to enable
to offer its services (as stated in its
postcondition). Hence, the precondition of a component is stated in its
requires-interfaces. Analogously to the above single sentence formulation of
a contract, we can state:
If the user of a component fulfils the component's requires-interface
(offers the right environment) the component will offer its services as
described in the provides-interface.
Let's denote with
the precondition of a component
and with
the postcondition of a component
. For checking check whether a
component
can be replaced safely by a component
, one has to ensure
that the contract of
is a subcontract of
. The notion of a subcontract
is described in [, p. 573] like contravariant typing for methods:
A contract
is a subcontract of contract
iff
 |
(2.1) |
(Where
means ``stronger'', i.e., if
and
are
predicates,
is
. In the set semantics of pre- and
postcondition below,
is the inclusion
.)
To check the interoperability between components
and
(see point (1)
in figure 2.7), one has to check whether
 |
(2.2) |
Coming back to protocol-modelling interfaces, we can consider the precondition
of a component as the set of required method call sequences, while the
postcondition is the set of offered call sequences. In this case, the checks
described in the above formulas (2.1) and (2.2) boiled
down to checking the inclusion relationship between the sets of call
sequences, i.e., for the substitutability check we have:
 |
(2.3) |
and for the interoperability check:
 |
(2.4) |
For arbitrary sets
and
holds
. Hence, the inclusion check we need for checking interoperability
and substitutability can be reduced to computing the intersection and
equivalence of sets of call sequences. One of the main reasons for choosing
finite state machines as a model to specify these sets of call sequences was
the existence of efficient algorithms for computing the intersection of two
FSMs and checking their equivalence. Of course, more powerful models than FSMs
exist (in the sense that they can describe protocols which cannot be
described by FSMs) but for many of these models (like the various push-down
automata) the equivalence is not decidable. Hence, one can use these models
for specifying component interfaces, but that does not help to check their
interoperbaility or substitutability at configuration-time.
Next: Parameterised Contracts as Generalisation
Up: Parametric Contracts
Previous: Parametric Contracts
Contents
Index
Snowball
2007-03-16