next up previous contents index
Next: Context Up: Parametric Contracts Previous: Interoperability Checks, Substitutability Checks   Contents   Index


Parameterised Contracts as Generalisation of Classical Contracts

While interoperability tests check the requires-interface of a component against the provides-interface of another component, parameterised contracts link the provides-interface of one component to the requires- interface of the same component (see points (2) and (3) in figure 2.7).

The usefulness of parameterised contracts is based on the observation that in practice often only a subset of a component's functionality is used. This is especially true for coarse-grained components. In this case, also only a subset of the functionality described in the requires-interface is actually used. That means that the component could be used without any problems in environments where not all dependencies, as described in the requires interface, are given. Vice versa, if a component does not receive all (but some) functionality it requires from the environment, it often can deliver a reasonable subset of its functionality.

Figure 2.7: Interoperability checks (1) and Requires-parameterised Contract (2) and Provides-parameterised Contract (3)
These facts can be modelled by a set of possible provides-interfaces $ \mathbf{P}:=\{prov\}$ and a set of possible requires-interfaces $ \mathbf{R}:=\{req\}$ and a monotone total bijective mapping $ p$ between them $ p:\mathbf{P}\rightarrow \mathbf{R}$.2.1 As a result, each requires-interface $ req\in \mathbf{R}$ is now a function of a provides-interface $ prov$: $ req = p(prov)$ and (because $ p$ is bijective) each provides-interface $ prov\in\mathbf{P}$ can be modelled as a function of a requires-interface $ req\in \mathbf{R}$: $ prov=p^{-1}(req)$.

This mapping $ p$ is now called parameterised contract, since it parameterises the precondition with the postcondition of the component and vice versa. It can be considered as a generalisation of ``classical contract'' which uses a fixed pre- and postcondition. The parameterised contract is bundled with the component and computes the interfaces of the components on demand.

For the following, assume component $ B$ uses component $ C$ and is used by component $ A$. If component $ A$ uses only a subset of the functionality offered by $ B$ we compute a new requires-interface of $ B$ with the parameterised contract $ p_B$:

$\displaystyle p_B(req_A\cap prov_B) =: req'_B \subseteq req_B$ (2.5)

Note that the new requires-interface $ req'_B$ requires possibly less than the original requires-interface $ req_B:=p_B(prov_B)$ (but never more) since $ p_B$ is monotone and $ req_A\cap prov_B\subseteq prov_B$. When computing the requires-interface out of a provides-interface (possibly intersected with an external requires-interface) the parameterised contract is called provides-parameterised contract.

Likewise, if component $ C$ does not provide all the functionality required by $ B$, one can compute a new provides-interface $ prov'_B$ with $ p_B$:

$\displaystyle p_B^{-1}(req_B\cap prov_C) =: prov'_B \subseteq prov_B$ (2.6)

Since $ p_B$ is monotone, $ p^{-1}$ is, too. With $ req_B\cap prov_C\subseteq
req_B$ we have $ prov'_B \subseteq prov_B:=p^{-1}(req_B)$. In this case we use a requires-parameterised contract.
next up previous contents index
Next: Context Up: Parametric Contracts Previous: Interoperability Checks, Substitutability Checks   Contents   Index
Snowball 2007-03-16