next up previous contents index
Next: Parameterised Contracts as Generalisation Up: Parametric Contracts Previous: Parametric Contracts   Contents   Index

Interoperability Checks, Substitutability Checks and Classical Contracts for Software Components

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: 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 $ C$ is the set of all components connected to $ C$'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 $ C$ is acting as a supplier and the environment as a client. The component $ C$ offers services to the environment (i.e., the components connected to $ C$'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 $ C$ expects from its environment (actually all components connected to $ C$'s requires-interface(s)) to be provided by the environment, in order to enable $ C$ 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 $ pre_c$ the precondition of a component $ c$ and with $ post_c$ the postcondition of a component $ c$. For checking check whether a component $ c$ can be replaced safely by a component $ c'$, one has to ensure that the contract of $ c'$ is a subcontract of $ c$. The notion of a subcontract is described in [, p. 573] like contravariant typing for methods: A contract $ c'$ is a subcontract of contract $ c$ iff

$\displaystyle pre_{c'} \trianglelefteq pre_c \wedge post_{c'} \trianglerighteq post_c$ (2.1)

(Where $ \trianglerighteq $ means ``stronger'', i.e., if $ pre_c$ and $ post_c$ are predicates, $ \trianglerighteq $ is $ \Rightarrow$. In the set semantics of pre- and postcondition below, $ \trianglerighteq $ is the inclusion $ \supseteq$.)

To check the interoperability between components $ c$ and $ c'$ (see point (1) in figure 2.7), one has to check whether

$\displaystyle pre_c \trianglelefteq post_{c'}$ (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:

$\displaystyle pre_{c'} \subseteq pre_c \wedge post_{c'} \supseteq post_c$ (2.3)

and for the interoperability check:

$\displaystyle pre_c \subseteq post_{c'}$ (2.4)

For arbitrary sets $ A$ and $ B$ holds $ A \subseteq B \Longleftrightarrow A
\cap B = A $. 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 up previous contents index
Next: Parameterised Contracts as Generalisation Up: Parametric Contracts Previous: Parametric Contracts   Contents   Index
Snowball 2007-03-16