Preserving Contract Satisfiability Under Non-monotonic Composition

Abstract

A contracts theory embeds non-monotonic composition (with respect to implementation) if the fact that a composition of two components implements a specification $\mathcal {S}$ does not generally follow from one of these components implementing $\mathcal {S}$. In contrast to monotonic composition, non-monotonic composition offers the additional expressiveness of specifying properties that only hold locally for a component since non-monotonic composition does not enforce all properties to be preserved when composing. Despite that this additional expressiveness is clearly needed, it implies that cases where monotony is indeed desired needs to be managed explicitly. The present paper elaborates on this topic by introducing a contracts theory embedding non-monotonic composition, and exploring conditions for ensuring monotonic composition in the context of this theory.

A  Propositions and Lemmas

The following two lemmas are used to prove Propositions 1 and 2, which follow after the lemmas.

Lemma 2

For any two sets of variables X and Y, it holds that

Proof

Consider an arbitrary . In accordance with Definition 3, this means that $\exists \mu \, . \, \omega [Y] = \mu [Y] \wedge \mu \in \{ \omega '\in \varOmega | \omega '[X] = \nu [X], \nu \in \mathsf {B}\}$. This can be rewritten as $\exists \nu \exists \mu \, . \, \omega [Y] = \mu [Y] \wedge \mu [X]= \nu [X] \wedge \nu \in \mathsf {B}$. Since $X\cap Y \subseteq X$ and $X\cap Y \subseteq Y$, and $\mu [X]= \nu [X]$ and $\omega [Y] = \mu [Y]$, it holds that $\mu [X\cap Y]= \nu [X\cap Y]$ and $\omega [X\cap Y] = \mu [X\cap Y]$, which also means that $\omega [X\cap Y]=\nu [X\cap Y]$. Thus, it holds $\exists \nu \, . \, \omega [X\cap Y] = \nu [X\cap Y] \wedge \nu \in \mathsf {B}$. In accordance with Definition 3, this means that . Since $\omega$ represents an arbitrary run in , it must hold that each run in is also in , which means that .

Next consider an arbitrary . In accordance with Definition 3, this means that $\exists \nu \, . \, \omega [X\cap Y] = \nu [X\cap Y] \wedge \nu \in \mathsf {B}$. Create a run $\mu$ such that $\mu [X]= \nu [X]$ and $\mu [X^\mathsf {C}] = \omega [X^\mathsf {C}]$. Since $\mu [X^\mathsf {C}] = \omega [X^\mathsf {C}]$, $\omega [X\cap Y] = \nu [X\cap Y]$, and $Y\subseteq X^\mathsf {C}\cup (X\cap Y)$, it follows that $\omega [Y] = \mu [Y]$. Thus, we have shown that $\exists \nu \exists \mu \, . \, \omega [Y] = \mu [Y] \wedge \mu [X]= \nu [X] \wedge \nu \in \mathsf {B}$, which can, as previously mentioned, be rewritten as $\exists \mu \, . \, \omega [Y] = \mu [Y] \wedge \mu \in \{ \omega '\in \varOmega | \omega '[X] = \nu [X], \nu \in \mathsf {B}\}$. In accordance with Definition 3, this means that . Since $\omega$ represents an arbitrary run in , it must hold that each run in is also in , which means that . Since it was previously also shown that , it follows that , which ends the proof.   $\square$

Lemma 3

It holds that .

Proof

In accordance with Definition 4, it holds that for each variable in $X^\mathsf {C}_{\mathsf {B}}=\{x_1,\ldots ,x_N\}$. It follows that

It follows in accordance with Lemma 2 that and since $X_{\mathsf {B}}=\{x_1\}^{\mathsf {C}}\cap \ldots \cap \{x_N\}^{\mathsf {C}}$, it also holds that , which ends the proof.   $\square$

Proposition 1

Let $\mathsf {B}_1$ and $\mathsf {B}_2$ be two behaviors such that $X_{\mathsf {B}_1} \cap X_{\mathsf {B}_2} = \emptyset$. Then, for an arbitrary set of variables Y, it holds

Proof

To prove , assume . According to Definition 3, this means that there exist a $\nu \in (\mathsf {B}_1 \cap \mathsf {B}_2)$ such that $\nu [Y] = \omega [Y]$. Thus for $i=1,2$, it holds that $\nu \in \mathsf {B}_i$ and $\nu [Y] = \omega [Y]$, and therefore that , which ends the proof.

To prove also that , consider an arbitrary run . According to Definition 3 this means that:

$$\begin{aligned}&\exists \nu _1 \in \mathsf {\mathsf {B}_1} . \nu _1[Y] = \omega [Y] \\&\exists \nu _2 \in \mathsf {\mathsf {B}_2} . \nu _2[Y] = \omega [Y] \end{aligned}$$

Now consider the vector $\nu =( \nu _1[X_{\mathsf {B}_1}], \nu _2[X^C_{\mathsf {B}_1}])$. Clearly it holds that $\omega [Y]=\nu [Y]$.

Since $\nu _1 \in \mathsf {B}_1$, and $\nu [X_{\mathsf {B}_1}] = \nu _1[X_{\mathsf {B}_1}]$, it holds according to Definition 3 that . Then, according to Lemma 3, it also holds that $\nu _1 \in \mathsf {B}_1$. Similarly, since $\nu _2 \in \mathsf {B}_2$, and $\nu [X_{\mathsf {B}_2}] = \nu _2[X_{\mathsf {B}_2}]$, it must hold that $\nu \in \mathsf {B}_2$.

Thus, we have shown that $\nu \in \mathsf {B}_1 \cap \mathsf {B}_2$ and that $\omega [Y]=\nu [Y]$. Therefore, according to Definition 3, it holds that , which ends the proof.   $\square$

Proposition 2

It holds that if $Y\cap X_{\mathsf {B}}\ne \emptyset$.

Proof

In accordance with Lemma 3, it holds that , and further that in accordance with Lemma 2. If $Y\cap X_{\mathsf {B}}\ne \emptyset$, it follows that .    $\square$

The following two lemmas are used to prove Theorem 2.

Lemma 4

If a behavior set $\mathcal {Q}$ is agnostic to a variable set X, then it is also agnostic to any variable set $Y \subseteq X$.

Proof

Consider a $\mathsf {B} \in \mathcal {Q}$ and a $\mathsf {B}'$ such that . Since $X^C \subseteq Y^C$, it holds according to Lemma 2, that

From this equality and since $\mathcal {Q}$ is agnostic to X, it follows that $\mathsf {B}'\in \mathcal {Q}$. Thus, we have shown that $\mathcal {Q}$ is agnostic to also Y.    $\square$

Lemma 5

Given two behaviors $\mathsf {B}$ and $\mathsf {B}'$ where $\mathsf {B}\cap \mathsf {B}'\ne \emptyset$, it holds that $X_{\mathsf {B}\cap \mathsf {B}'}\subseteq X_{\mathsf {B}}\cup X_{\mathsf {B}'}$.

Proof

Assume $X_{\mathsf {B}\cap \mathsf {B}'}\nsubseteq X_{\mathsf {B}}\cup X_{\mathsf {B}'}$, which will be shown to lead to a contradiction. This means that there exists an x such that $x\notin X_{\mathsf {B}}$, $x\notin X_{\mathsf {B}'}$, and $x\in X_{\mathsf {B}\cap \mathsf {B}'}$. In accordance with Definition 4, this respectively means that

(12)

(13)

(14)

Proposition 1 and (14) imply , which in combination with (12) and (13) imply that $\mathsf {B}\cap \mathsf {B}'\ne \mathsf {B}\cap \mathsf {B}'$. Since this is a contradiction, assumption $X_{\mathsf {B}\cap \mathsf {B}'}\nsubseteq X_{\mathsf {B}}\cup X_{\mathsf {B}'}$ must be false, and it must rather hold that $X_{\mathsf {B}\cap \mathsf {B}'}\subseteq X_{\mathsf {B}}\cup X_{\mathsf {B}'}$, which completes the proof.    $\square$