# Preserving Contract Satisfiability Under Non-monotonic Composition

Jonas Westman, Mattias Nyberg

► To cite this version:

Jonas Westman, Mattias Nyberg. Preserving Contract Satisfiability Under Non-monotonic Composition. 38th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2018, Madrid, Spain. pp.181-195, 10.1007/978-3-319-92612-4_10. hal-01824811

HAL Id: hal-01824811

https://inria.hal.science/hal-01824811

Submitted on 27 Jun 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Preserving Contract Satisfiability under
Non-Monotonic Composition

Jonas Westman¹ and Mattias Nyberg¹²

¹ Royal Institute of Technology (KTH), Stockholm, Sweden
jowestm@kth.se

² Scania, Södertälje, Sweden

**Abstract.** A contracts theory embeds *non-monotonic composition* (with respect to implementation) if the fact that a composition of two components implements a specification *S* does not generally follow from one of these components implementing *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.

**Keywords:** Contracts, Non-monotonic, Composition, Satisfiability

# 1 Introduction

The notion of *contracts* was first introduced in [10] as a pair of pre- and post-
conditions [8] to be used in formal specification of software (SW) *components*.
More recent, general contracts theories [2, 6, 9, 11–13] consider a wider notion of
a contract applicable for components in any domain (SW, hardware, physical,
etc.). In such general theories, a contract ($\mathcal{A}, \mathcal{G}$) expresses a commitment of a
component to guarantee the *implementation* of a specified property $\mathcal{G}$, given
that the component is *composed* with an environment implementing a specified
property $\mathcal{A}$.

More concretely, despite using different terminology and notation, such gen-
eral contracts theories [2, 6, 9, 11–13] are all grounded in the following concepts:

- component $C$;

- composition $\times$ on pairs of components;

- specification $S$; and

- implementation relation $\models$ on components and specifications.

Defined from these concepts, a contract is a pair $(\mathcal{A}, \mathcal{G})$ of specifications and is
*satisfied* by a component $C$ if $E \times C \models \mathcal{G}$ for each component $E \models \mathcal{A}$.
Another common characteristic of general contracts theories [2, 6, 9, 11–13] is that they embed *monotonic composition* (with respect to implementation), i.e.

$$ C \models S \Rightarrow \forall C'. C' \times C \models S. \qquad (1) $$

An example is the theory in [2] where components and specifications both are characterized by *assertions*, i.e., sets of value sequences, over the same (universal) set of variables. Composition $\times$ and implementation $\models$ are instantiated by $\cap$ and $\subseteq$, respectively, which means that (1) translates to $C \subseteq S \Rightarrow \forall C'. C' \cap C \subseteq S$, which generally holds.

Despite previous general contracts theories [2, 6, 9, 11–13] embedding *monotonic composition*, there is at least one strong reason why a general contracts theory by itself should not enforce (1), i.e., why a contracts theory should embed *non-monotonic composition* instead.

This reason is that theories embedding monotonic composition is inherently limited to specification of properties that are preserved through composition. Formulated differently, a theory with monotonic composition does not support specifying properties that *only* hold locally for a component since all properties are preserved when composing. This means that it is not possible to express, e.g., that a component *shall not* constrain a variable $x$ to any particular value, but that the composition of this component and another *shall* constrain $x$. In an engineering context, this could correspond to a specification expressing that "a subsystem shall not send out a particular signal" – a property that will not be preserved when composed with a component that sends out the signal.

Thus, in contrast to embedding monotonic composition, embedding non-monotonic composition in a contracts theory offers the additional expressiveness of specifying purely local properties. Despite that this additional expressiveness is clearly needed, there are many cases where we do want composition to be monotonic with respect to implementation. Since a theory embedding non-monotonic composition does not ensure this by itself, in such a theory, it is necessary to understand the conditions for when composition is monotonic and when it is not.

More explicitly, in a theory embedding non-monotonic composition, consider that the guarantee of a contract $(A, G)$ expresses a property intended to be *global*, i.e. always preserved through composition. If a component $C$ satisfying $(A, G)$ is first composed with a component $E \models A$, it follows that $E \times C \models G$; however, if $E \times C$ is later composed with another component $C'$, it does not generally follow that $C' \times E \times C \models G$, and thus, this has to be ensured explicitly. More generally, independent of the order in which components are composed, it needs to be ensured that for each $E \models A$ and $C$ satisfying $(A, G)$, it holds that $C' \times E \times C \models G$, which is equivalent to

$$ \forall C. (C \text{ satisfies } (A, G) \Rightarrow C' \times C \text{ satisfies } (A, G)). \qquad (2) $$

Since (2) is not embedded in a contracts theory with non-monotonic composition, ensuring (2) needs to be done explicitly. The present paper elaborates on
this topic by introducing a contracts theory embedding non-monotonic composition, and exploring conditions for ensuring (2) in the context of this theory.

The introduction of this contracts theory constitutes a first contribution. Similar to the previously exemplified theory [2], in the introduced theory, components are characterized by assertions and composition is set intersection; however, in contrast to [2], specifications are sets of assertions instead of just assertions, and implementation is instantiated by $\in$ instead of $\subseteq$. The proposed theory embeds non-monotonic composition since (1) instantiates to $C \in S => \forall C'$. $C' \cap C \in S$, which clearly does not generally hold.

As a second contribution, conditions for ensuring (2) are presented. This includes a sufficient condition, which is that component $C'$ satisfies contract $(G|G)$. It is shown that this condition is in fact also necessary if, for each $G \in G$, there exists a component that satisfies $(A, \{G\})$. Furthermore, it shown that monotonic composition with respect to composition can also be ensured by a condition based on having components $C, C'$, and each $E \in A$ implement special types of specifications, called *interface port specifications*, which ensure that the set of variables constrained by components $C'$ and $E \cap C$ are respectively disjoint, and thus, that the components are isolated from each other.

As previously mentioned, general contracts theories [2, 6, 9, 11–13] all embedded monotonic composition, instead of non-monotonic composition as in the contracts theory presented in this paper. However, there are contracts meta theories [1,3] that are not limited to monotonic composition. More specifically, these meta theories support instantiating theories embedding non-monotonic composition, but also contracts theories embedding monotonic composition. Thus, these meta theories are defined at a level agnostic to whether composition is monotonic or non-monotonic, which means that these meta theories naturally do not support reasoning about properties that are specific to contracts theories embedding non-monotonic composition. In contrast, the present paper studies the concept of non-monotonic composition in depth, presenting several theorems and propositions manifesting properties inherent to this concept.

The rest of the paper is organized as follows. Section 2 presents established concepts from previous contracts theories. Section 3 introduces, as a first contribution, a novel contracts theory where composition is non-monotonic with respect to implementation. Section 4 then presents, as a second contribution, conditions to ensure monotony of composition in this contracts theory. Section 5 summarizes the paper and draws conclusions.

## 2 Preliminaries

This section presents definitions already established in [13], which in turn draws on the contracts theory in [2].

Let $\Xi = \{x_1, \dots, x_N\}$ denote the set of variables considered, and we call this the *universal set* of variables. Similarly, let $T_{\ge 0} \subseteq \mathbb{R}$ denote the universal set of time points considered. $T_{\ge 0}$ can be defined to be a continuous, e.g. if $T_{\ge 0}$ is defined by $[0, 1000]$, or discrete, e.g. if $T_{\ge 0} = \{0.1 * n | n \in \{0, 1, 2, \dots, 10000\}\}$.
The time points in $T_{\ge 0}$ do not represent absolute time, but instead, time relative to the start of execution or observation of the system. Furthermore, $T_{\ge 0}$ contains 0 and no negative time points.

**Definition 1 (Run, see [13]).** A run $\omega = (x_1(t), \dots, x_N(t))$ is a vector valued function, with the elements being the variables in $\Xi$, and defined on a time subinterval $T^\omega \subseteq T_{\ge 0}$ starting at time 0, i.e. $0 \in T^\omega$. $\square$

For example, a run can be a trace [5,7,14] or an execution as presented in [11]. Note that two different runs may be defined on two different time intervals.

Let $\Omega$ denote the set of all possible runs.

**Definition 2 (Behavior, see [13]).** A behavior B is a, possibly empty, set of runs. $\square$

This notion corresponds to an assertion as presented in [2, 4].

*Example 1.* Consider a universal set of variables $\Xi = \{x, y\}$. Examples of runs are $\omega_1 = (x(t), y(t)) = (t, e^t)$ and $\omega_2 = (t, 2e^t)$ defined on an interval $T^\omega = [0, 10]$. These two runs can be combined to form four different behaviors $B_1 = \{\}, B_2 = \{(t, e^t)\}, B_3 = \{(t, 2e^t)\},$ and $B_4 = \{(t, e^t), (t, 2e^t)\}$. $\square$

*Example 2.* Let $\Xi = \{x, y\}$ where $x$ and $y$ are Boolean variables and $T^\omega = \{0\}$ for all runs. Examples of behaviors are $B_1 = \{(0, 0)\}$, $B_2 = \{(0, 1)\}$, $B_3 = \{(0, 0), (0, 1)\}$, and $B_4 = \{(0, 0), (1, 1)\}$. $\square$

Let $\omega[X]$ denote the subvector of $\omega$ having the variables $X \subseteq \Xi$. For example, if $\Xi = \{a, b, c, d\}$, then $\omega[\{b, d\}] = (b, d)$. If $X = \emptyset$, then let $\omega[X] = \emptyset$.

**Definition 3 (Projection, see [13]).** The projection of behavior B onto a set of variables $X \subseteq \Xi$, denoted $\text{proj}_X B$, is the set of runs:

$$ \{\omega \in \Omega \mid \exists \nu \in B. \nu[X] = \omega[X]\}. \quad \square $$

Note that projection is called extended projection in [13] and is defined using slightly different notation. Note also that if $B \neq \emptyset$, then $\text{proj}_\emptyset B = \Omega$ and $\text{proj}_\Xi B = B$. Furthermore, for any variable set $Y$, it holds $\text{proj}_Y \emptyset = \emptyset$ and $\text{proj}_Y \Omega = \Omega$.

*Example 3.* For the behaviors defined in Example 2, it holds that $\text{proj}_{\{x\}} B_1 = \text{proj}_{\{x\}} B_2 = \{(0, 0), (0, 1)\}$ and $\text{proj}_{\{x\}} B_3 = B_3$, and $\text{proj}_{\{x\}} B_4 = \Omega$. $\square$

Let $\{x\}^C$ denote the complement set of $\{x\}$, i.e. $\{x\}^C = \Xi \setminus \{x\}$.

**Definition 4 (Behavior Constrains, see [13]).** A behavior B constrains a variable $x$ if

$$ \text{proj}_{\{x\}}^C B \neq B. \quad \square $$

Let $X_B$ denote the set of variables constrained by B. Note that $X_\Omega = \emptyset$ and $X_\emptyset = \emptyset$.
*Example 4.* For the behaviors discussed in Example 2 and Example 3, it holds $\{y\}^c = \{x\}$. Furthermore, $\text{proj}_{\{y\}}^c B_1 = \text{proj}_{\{x\}} B_1 \neq B_1$. Therefore $B_1$ constrains $x$. In fact, $B_1$ also constrains $y$, and therefore $X_{B_1} = \{x, y\}$.

Since $\text{proj}_{\{x\}} B_3 = B_3$, it holds that $B_3$ does not constrain $y$. However, behavior $B_3$ does constrain $x$ since $\text{proj}_{\{y\}} B_3 = \{(0,0), (0,1), (1,0), (1,1)\} \neq B_3$. $\square$

# 3 Composition, Specifications, and Contracts

Based upon the definition of behavior in Section 2 and as the first contribution of the paper, this section presents the basis of a contracts theory in which specifications are represented as sets of behaviors. The achievement is a theory where composition is non-monotonous with respect to implementation of specifications.

## 3.1 Composition

We assume that each component is characterized by a behavior. When two components, characterized by behaviors $B_1$ and $B_2$ respectively, are put together, we assume that a new behavior, called the composition of $B_1$ and $B_2$, is formed and that it conforms to the following definition.

**Definition 5 (Composition of Behaviors).** The composition of two behaviors $B_1$ and $B_2$ is their intersection $B_1 \cap B_2$. $\square$

## 3.2 Specifications

A specification $S$ expresses an intended property of a component. Commonly such an intended property is called a 'requirement'. If a behavior implements a specification, then this really means that the component characterized by the behavior has the intended property expressed by $S$. These notions are now formalized in the following two definitions.

**Definition 6 (Specification).** A specification $S$ is a, possibly empty, set of behaviors. $\square$

**Definition 7 (Behavior Implements Specification).** A behavior $B$ implements a specification $S$ if $B \in S$. $\square$

Note that the empty set $\emptyset$ can be a specification, and considering that $\emptyset$ can also be a behavior, the set $\{\emptyset\}$ can be a specification.

*Example 5.* Let $\Xi = \{x, y\}$ and $T^\omega = \{0\}$. Then

$$S = \{((0,0), (0,1)), ((0,1)), ((0,0), (1,1))\}$$

is a possible specification. Behavior $B_3 = \{(0,0), (0,1)\}$ implements $S$ and also $B_4 = \{(0,0), (1,1)\}$ implements $S$. However, the composition $B_3 \cap \{(0,0), (1,1)\} = \{(0,0)\}$ does not implement $S$. $\square$

Example 5 highlights the fact that even though the two behaviors $B_3$ and $B_3$ individually implement the specification $S$, their composition does not. That is, composition is non-monotonic with respect to implementation of specification.
### 3.3 Contracts

In alignment with the notion of contract and satisfy as introduced in Section 1, this section presents the instantiation resulting from the definitions of specification and implementation presented in Section 3.2.

A contract is a pair $(\mathcal{A}, \mathcal{G})$ of specifications expressing an intended property of a composition of two behaviors E and B where $E \in \mathcal{A}$.

**Definition 8 (Contract).** A contract is a pair $(\mathcal{A}, \mathcal{G})$ of specifications, where:

(i) $\mathcal{G}$ is non-empty and called *guarantee*; and
(ii) $\mathcal{A}$ is possibly empty and called *assumption*. $\square$

**Definition 9 (Behavior Satisfies Contract).** A behavior B satisfies a contract $(\mathcal{A}, \mathcal{G})$ if, for each E implementing $\mathcal{A}$, it holds that the composition $E \cap B$ implements $\mathcal{G}$. $\square$

If the instantiations of specification and implements are written out, we obtain that a behavior B satisfies a contract $(\mathcal{A}, \mathcal{G})$ if, and only if,

$$ \forall A \in \mathcal{A}. A \cap B \in \mathcal{G} \qquad (3) $$

Note that a contract $(\mathcal{A}, \mathcal{G})$ is trivially satisfied if $\mathcal{A} = \emptyset$.

### 3.4 Specification is Agnostic to Set of Variables

As discussed above, a consequence of Definitions 6 and 7 of specification and implements is that composition is not inherently monotonic with respect to implementation. However, in many cases monotony is indeed desirable. One such case is when a specification represents an intended relation on a proper subset of the universal set $\Xi$. An example is when $S_1$ expresses an intended property $x = 0$ and where $x \subset \Xi$. Consider a first component that itself implements $S_1$ by setting $x = 0$ and not constraining any other variables. If this first component is composed with a second component that does not in any way constrain $x$, then we should expect that their composition also implements $S_1$. As a fundamental concept to support such reasoning, we introduce the notion of *agnostic specification*:

**Definition 10 (Specification is Agnostic to Set of Variables).** A specification $S$ is agnostic to a set of variables $X$ if

$$ \forall B \in S. (\forall B'. \text{proj}_{X^c} B' = \text{proj}_{X^c} B \Rightarrow B' \in S). \quad \square $$

A specification is agnostic to a set of variables $X$ if the fact whether or not a behavior implements the specification is independent on whether or not the behavior constrains variables in $X$.

*Example 6.* Let $\Xi = \{x, y\}$ where $x$ and $y$ are Boolean variables and $T^\omega = \{0\}$. Two examples of specifications that are agnostic to $\{y\}$ are:
$$- \{ \{(0,0)\}, \{(0,1)\}, \{(0,0), (0,1)\} \}$$

$$- \{ \{(0,0)\}, \{(0,1)\}, \{(0,0), (0,1)\}, \{(1,1)\}, \{(1,0)\}, \{(1,0), (1,1)\} \}.$$

Any proper subset of these behavior sets are not agnostic to {$y$}. Three such examples are:

$$- \{ \{(0,0)\} \}$$

$$- \{ \{(0,0)\}, \{(0,1)\} \}$$

$$- \{ \{(0,0), (0,1), (1,0), (1,1)\} \}.$$

□

Now, to illustrate how the concept of agnostic specification can be used to ensure monotonic composition with respect to implementation of specification, consider again the previously introduced specification $S_1$. Assume that $S_1$, expressed by $x = 0$, is agnostic to {$y$}. Since the first component implements $S_1$, it holds $B_1 \in S_1$. Also, since the first component does not constrain any other variables than $x$, it holds that $B_1$ does not constrain $y$. For any behavior $B_2$ constraining only $y$, it holds $\text{proj}_{\{x\}} B_2 = \Omega$ (see Proposition 2 in Appendix A). Next, we will use the following proposition with proof given in Appendix A:

**Proposition 1.** Let $B_1$ and $B_2$ be two behaviors such that $X_{B_1} \cap X_{B_2} = \emptyset$. Then, for an arbitrary set of variables $Y$, it holds

$$\text{proj}_Y(B_1 \cap B_2) = \text{proj}_Y B_1 \cap \text{proj}_Y B_2 .$$

□

By using Proposition 1, we derive that

$$\text{proj}_{\{x\}}(B_1 \cap B_2) = \text{proj}_{\{x\}} B_1 \cap \text{proj}_{\{x\}} B_2 = \text{proj}_{\{x\}} B_1 \cap \Omega = \text{proj}_{\{x\}} B_1 \quad (4)$$

Specification $S_1$ being agnostic to {$y$} means according to Definition 10 that

$$\forall B'. \text{proj}_{\{x\}} B' = \text{proj}_{\{x\}} B_1 \Rightarrow B' \in S_1 \quad (5)$$

Combining (4) and (5), implies that the composition $B' = B_1 \cap B_2 \in S_1$.

In summary, the fact is that since $S_1$, expressing $x = 0$, is agnostic to $y$, the composition of any behavior in $S_1$ with any other behavior that only constrains $y$ will result in a behavior also in $S_1$. This fact will be generalized in Section 4.3 presenting a similar condition, but in terms of satisfying a contract instead of implementing a specification.

# 4 Preserving Contract Satisfiability Under non-Monotonic Composition

Section 3 presented a contracts theory where components are characterized by behaviors, composition is set intersection, specifications are behavior sets, and implementation is defined by $\in$. As previously mentioned in Section 1, the proposed theory embeds non-monotonic composition since (1) instantiates to $B \in S \Rightarrow \forall B'$. $B' \cap B \in S$, which clearly does not generally hold. As also stated
in Section 1, this means that it follows that (2) also does not hold, i.e., it does not hold that

$$ \forall B. B \text{ satisfies } (A, G) \Rightarrow B' \cap B \text{ satisfies } (A, G). \qquad (6) $$

However, ensuring (6) is desirable for any use-case where $G$ expresses a property that is intended to be implemented by a composition of $B'$ and the composition $B \cap E$ of a component $B$ satisfying $(A, G)$ and a component $E \in A$.

In order to be able to support such use-cases, this section now proceeds to present conditions for ensuring (6). This includes a sufficient and necessary condition of (6); however, to gradually introduce this condition to the reader, a condition is first presented that is only sufficient and not necessary, but that is less technical and directly follows from the necessary and sufficient condition.

## 4.1 Sufficient Condition for Preserving Satisfiability

Consider constructing a contract $(A', G')$ for component $B'$ such that (6) is ensured if $B'$ satisfies the contract. Since $G'$ is intended to express a property of the composition of $B'$ and a behavior $A \in A'$, and $G$ is to be implemented by the composition, it makes sense that $G' = G$. Regarding the assumption $A'$, to enforce that the composition of $B'$ and any behavior implementing $G$ also implements $G$, each behavior implementing $G$ should be in $A'$. Since $G$ contains each behavior implementing it, it also makes sense that $A' = G$. Indeed, as shown in the following corollary, if $B'$ satisfies $(G, G)$, then (6) holds.

**Corollary 1.** Given a contract $(A, G)$, if a behavior $B'$ satisfies $(G, G)$, then

$$ \forall B. B \text{ satisfies } (A, G) \Rightarrow B' \cap B \text{ satisfies } (A, G). $$

*Proof.* This corollary follows from Theorem 1 in Section 4.2 since Definition 11 implies that $R_G(A, G) \subseteq G$, which means, in accordance with (3), that: $B'$ satisfies $(G, G) \Rightarrow B'$ satisfies $(R_G(A, G), G)$. $\square$

*Example 7.* Let $\Xi = \{x, y\}$ where $x$ and $y$ are Boolean variables and $T^\omega = \{0\}$. Consider a contract $(A, G)$ where $A = \{A_1, A_2\} = \{\{(0, 0)\}, \{(0, 0), (0, 1)\}\}$ and $G = \{G_1, G_2, G_3\} = \{\{(0, 0)\}, \{(1, 0)\}, \{(0, 0), (1, 0)\}\}$.

Behavior $B = \{(0, 0), (1, 1)\}$ satisfies the contract $(A, G)$ since

$$ A_1 \cap B = \{(0, 0)\} \cap \{(0, 0), (1, 1)\} = \{(0, 0)\} = G_1 \in G $$

$$ A_2 \cap B = \{(0, 0), (0, 1)\} \cap \{(0, 0), (1, 1)\} = \{(0, 0)\} = G_1 \in G. $$

Behavior $B'_1 = \{(0, 0), (1, 0), (1, 1)\}$ satisfies the contract $(G, G)$ since

$$ G_1 \cap B'_1 = \{(0, 0)\} \cap \{(0, 0), (1, 0), (1, 1)\} = \{(0, 0)\} = G_1 \in G $$

$$ G_2 \cap B'_1 = \{(1, 0)\} \cap \{(0, 0), (1, 0), (1, 1)\} = \{(1, 0)\} = G_2 \in G $$

$$ G_3 \cap B'_1 = \{(0, 0), (1, 0)\} \cap \{(0, 0), (1, 0), (1, 1)\} = \{(0, 0), (1, 0)\} = G_3 \in G. $$
Then, in agreement with Corollary 1, composition $B'_1 \cap B$ satisfies $(A, G)$ since

$$A_1 \cap B'_1 \cap B = \{(0,0)\} \cap \{(0,0), (1,0), (1,1)\} \cap \{(0,0), (1,1)\} = \{(0,0)\} = G_1 \in G \\ A_2 \cap B'_1 \cap B = \{(0,0), (0,1)\} \cap \{(0,0), (1,0), (1,1)\} \cap \{(0,0), (1,1)\} = \{(0,0)\} = G_1 \in G.$$

On the other hand, the behavior $B'_2 = \{(0,1), (1,0), (1,1)\}$ does not satisfy the contract $(G, G)$ since

$$G_1 \cap B'_2 = \{(0,0)\} \cap \{(0,1), (1,0), (1,1)\} = \emptyset \notin G.$$

Also so we see that the composition $B'_2 \cap B$ does not satisfy $(A, G)$ since

$$A_1 \cap B'_2 \cap B = \{(0,0)\} \cap \{(0,1), (1,0), (1,1)\} \cap \{(0,0), (1,1)\} = \emptyset \notin G. \quad \square$$

## 4.2 Necessary and Sufficient Condition for Preserving Satisfiability

Section 4.1 presented Corollary 1 expressing a condition for ensuring (6). As previously mentioned, this condition is a sufficient, but not necessary condition of (6).

This is due to the fact that the assumption in the contract $(G, G)$ may include behaviors that cannot be a composition of a behavior satisfying $(A, G)$ and a behavior $A \in A$. The subset of $G$ obtained by removing such behaviors from $G$ is here called the *realizable guarantee of* $(A, G)$.

**Definition 11 (Realizable Guarantee of Contract).** The realizable guarantee of a contract $(A, G)$, denoted $R_G(A, G)$, is the specification $\{A \cap B \mid A \in A \wedge B \text{ satisfies } (A, G)\}$. $\square$

As expressed in the following proposition, contracts $(A, G)$ and $(A, R_G(A, G))$ are satisfied by the exact same behaviors.

**Proposition 2.** A behavior satisfies a contract $(A, G)$ if and only if the behavior satisfies $(A, R_G(A, G))$. $\square$

*Proof.* Follows directly from (3) and Definition 11. $\square$

Having $B'$ satisfy $(R_G(A, G), G)$ instead of $(G, G)$ is indeed sufficient for ensuring (6). The behaviors in $G \setminus R_G(A, G)$ are not compositions of a behavior $B$ satisfying $(A, G)$ and a behavior $A \in A$; therefore, these behaviors can be excluded from the assumption of $(G, G)$ since the implication in (6) is trivially true for any behavior $B$ that does not satisfy $(A, G)$. The following theorem not only shows that it is indeed the case that $B'$ satisfying $(R_G(A, G), G)$ is sufficient for ensuring (6), but that this is in fact also a necessary condition.

**Theorem 1.** Given a contract $(A, G)$, a behavior $B'$ satisfies $(R_G(A, G), G)$ if and only if:

$$\forall B. B \text{ satisfies } (A, G) \Rightarrow B' \cap B \text{ satisfies } (A, G). \quad (7)$$
The proof of Theorem 1 follows after the following lemma.

**Lemma 1.** A behavior satisfies a contract ($\mathcal{A}_1 \cup \dots \cup \mathcal{A}_N, \mathcal{G}$) if the behavior satisfies each contract ($\mathcal{A}_i, \mathcal{G}$).

*Proof of Lemma 1.* In accordance with (3), consider as given a behavior B such that $\forall A_i \in \mathcal{A}_i.A_i \cap B \in \mathcal{G}$. It follows directly that $\forall A \in (\mathcal{A}_1 \cup \dots \cup \mathcal{A}_N).A \cap B \in \mathcal{G}$, which means that B satisfies $(\mathcal{A}_1 \cup \dots \cup \mathcal{A}_N, \mathcal{G})$ in accordance with (3). $\square$

*Proof of Theorem 1.* For the if-only case, in accordance with (3), consider as given

$$ \forall A \in \mathcal{R}_G(\mathcal{A}, \mathcal{G}).A \cap B' \in \mathcal{G}. \qquad (8) $$

Consider an arbitrary behavior B that satisfies $(\mathcal{A}, \mathcal{G})$, which means that $\forall A \in \mathcal{A}.A \cap B \in \mathcal{R}_G(\mathcal{A}, \mathcal{G})$ in accordance with Proposition 2 and (3). This and (8) imply $\forall A \in \mathcal{A}.A \cap B \cap B' \in \mathcal{G}$, which means that $B' \cap B$ satisfies $(\mathcal{A}, \mathcal{G})$ in accordance with (3). This also holds for each B satisfying $(\mathcal{A}, \mathcal{G})$ since B characterizes an arbitrary behavior, and (7) hence holds.

For the if case, consider that (7) holds. It follows in accordance with (3) that

$$ \forall B.(B \text{ satisfies } (\mathcal{A}, \mathcal{G}) \Rightarrow (\forall A' \in \mathcal{A}.A' \cap B' \cap B \in \mathcal{G})). $$

Notably, $\forall A' \in \mathcal{A}.A' \cap B' \cap B \in \mathcal{G}$ can be rewritten as $\forall A \in \{A' \cap B | A' \in \mathcal{A}\}.A \cap B' \in \mathcal{G}$, which in accordance with (3) means that

$$ \forall B.B \text{ satisfies } (\mathcal{A}, \mathcal{G}) \Rightarrow B' \text{ satisfies } (\{A \cap B | A \in \mathcal{A}\}, \mathcal{G}). $$

This and Lemma 1 imply that $B'$ satisfies

$$ (\bigcup_{B,B \text{ satisfies } (\mathcal{A},\mathcal{G})} \{A \cap B | A \in \mathcal{A}\}, \mathcal{G}), $$

which is equivalent to $B'$ satisfying $(\{A \cap B | A \in \mathcal{A}, B \text{ satisfies } (\mathcal{A}, \mathcal{G})\}, \mathcal{G})$. In accordance with Definition 11, this means that $B'$ satisfies $(\mathcal{R}_G(\mathcal{A}, \mathcal{G}), \mathcal{G})$, which ends the proof. $\square$

## 4.3 Preserving Satisfiability through Interface Port Specifications

Similar to Sections 4.1 and 4.2, this section presents a condition for preserving contract satisfiability; however, in contrast to the conditions presented in Sections 4.1 and 4.2, rather than ensuring (6), this condition is sufficient for

$$ \forall B \in \mathcal{I}_X . B \text{ satisfies } (\mathcal{A}, \mathcal{G}) \Rightarrow B' \cap B \text{ satisfies } (\mathcal{A}, \mathcal{G}), \qquad (9) $$

where $\mathcal{I}_X = \{B | X_B \subseteq X\}$. In contrast to (6), which quantifies over each behavior, formula (9) quantifies over each behavior B that implements a special type of specification, here denoted $\mathcal{I}_X$ and called *interface port specification*, which expresses only a restriction on the set of variables that B can constrain.
**Definition 12 (Interface Port Specification).** An interface port specification for X is a specification $\{\mathbf{B} | X_{\mathbf{B}} \subseteq X\}$. □

Prior to presenting a theorem ensuring (9), an example will be studied.

*Example 8.* Consider $\Xi = \{x, y, u, v\}$ where $x, y, u$, and $v$ are Boolean variables and $T^w = \{0\}$. Let $\mathbf{B}'$ be a behavior and $(\mathcal{A}, \mathcal{G})$ a contract where:

a) $\mathbf{B}' = \{(x, y, u, v) \in \Omega \mid u = v\}$;

b) $\mathcal{G} = \{\mathbf{B} \neq \emptyset \mid \forall (x, y, u, v) \in \mathbf{B}. x = 1\}$; and

c) $\mathcal{A} = \{\mathbf{B} \mid \forall (x, y, u, v) \in \mathbf{B}. y = 1\} \cap \mathcal{I}_{\{x,y\}}$.

Consider a behavior $\mathbf{B} = \{(x, y, u, v) \in \Omega \mid x = y\}$, and an arbitrary behavior $\mathcal{A} \in \mathcal{A}$. Their intersection $\mathcal{A} \cap \mathbf{B}$ is behavior $\{(x, y, u, v) \in \Omega \mid x = y = 1\}$, which implements $\mathcal{G}$. This means that in order for (9) to hold, behavior $\mathbf{B}' \cap \mathcal{A} \cap \mathbf{B}$ must also implement $\mathcal{G}$. This is indeed the case since $\mathbf{B}' \cap \mathcal{A} \cap \mathbf{B} = \{(x, y, u, v) \in \Omega \mid x = y = 1 \text{ and } u = v\}$, contained in $\mathcal{G}$. □

In accordance with Definitions 10 and 12, conditions (a)-(c) in Example 8 respectively imply:

i) $\mathbf{B}' \in \mathcal{I}_{\{u,v\}}$;

ii) $\mathcal{G}$ is agnostic to $\{u, v, y\} \supseteq \{u, v\}$ and $\emptyset \notin \mathcal{G}$; and

iii) $\mathcal{A} \subseteq \mathcal{I}_{\{u,v\}^c}$.

As will be shown in the following theorem, conditions (i)-(iii) ensure that if a behavior $\mathbf{B}$ satisfies $(\mathcal{A}, \mathcal{G})$ and implements an interface specification for a set disjoint to $\{u, v\}$, e.g. $\{x, y\}$ as in Example 8, then it holds that $\mathbf{B}' \cap \mathcal{B}$ satisfies $(\mathcal{A}, \mathcal{G})$.

**Theorem 2.** Given a contract $(\mathcal{A}, \mathcal{G})$ and two disjoint sets of variables $X$ and $Y$, if

i) $\mathbf{B}' \in \mathcal{I}_Y$

ii) $\mathcal{G}$ is agnostic to a set $Z \supseteq Y$ and $\emptyset \notin \mathcal{G}$; and

iii) $\mathcal{A} \subseteq \mathcal{I}_{Y^c}$,

then it holds: $\forall \mathbf{B} \in \mathcal{I}_X$. $\mathbf{B}$ satisfies $(\mathcal{A}, \mathcal{G}) \Rightarrow \mathbf{B}' \cap \mathbf{B}$ satisfies $(\mathcal{A}, \mathcal{G})$.

The lemmas used in the following proof can be found in Appendix A.

*Proof.* Assume (i)-(iii), and an arbitrary behavior $\mathbf{B} \in \mathcal{I}_X$ satisfying $(\mathcal{A}, \mathcal{G})$, i.e., $\forall \mathcal{A} \in \mathcal{A}. \mathcal{A} \cap \mathbf{B} \in \mathcal{G}$ in accordance with (3). From (i), in accordance with Definition 12, it follows that $X_{\mathbf{B}'} \subseteq Y$. In accordance with Lemma 4, this and (ii) imply that $\mathcal{G}$ is agnostic to $X_{\mathbf{B}'}$. For an arbitrary $\mathcal{A} \in \mathcal{A}$, in accordance with Definition 10 and since $\mathcal{A} \cap \mathbf{B} \in \mathcal{G}$, it follows that

$$ (\mathrm{proj}_{X_{\mathbf{B}'}^c}(\mathbf{B}' \cap (\mathcal{A} \cap \mathbf{B}))) = (\mathrm{proj}_{X_{\mathbf{B}'}^c}(\mathcal{A} \cap \mathbf{B})) \Rightarrow \mathbf{B}' \cap (\mathcal{A} \cap \mathbf{B}) \in \mathcal{G}. \quad (10) $$
In accordance with Definition 12, $B \in \mathcal{I}_X$ and (iii) imply $X_B \subseteq X$ and $X_A \subseteq Y^C$, respectively. Since $X \cap Y = \emptyset$ was given, it follows that $X_B \subseteq Y^C$, and further that $X_A \cup X_B \subseteq Y^C$. Then in accordance with Lemma 5 and since $A \cap B \neq \emptyset$ due to $\emptyset \notin \mathcal{G}$ in (ii), it holds that $X_{A \cap B} \subseteq Y^C$, which means that $X_{A \cap B} \cap X_{B'} = \emptyset$ since $X_{B'} \subseteq Y$. In accordance with Proposition 1, this means that (10) is equivalent to

$$ (\mathrm{proj}_{X_{B'}}^{c}(B') \cap \mathrm{proj}_{X_{B'}}^{c}(A \cap B) = \mathrm{proj}_{X_{B'}}^{c}(A \cap B)) \Rightarrow B' \cap (A \cap B) \in \mathcal{G}. \quad (11) $$

In accordance with Lemma 2, it holds that $\mathrm{proj}_{X_{B'}}^{c}(B') = \Omega$, which means that the left side of the implication in (11) is equivalent to $\Omega \cap \mathrm{proj}_{X_{B'}}^{c}(A \cap B) = \mathrm{proj}_{X_{B'}}^{c}(A \cap B)$. Since $\Omega$ includes all runs, it follows that $\mathrm{proj}_{X_{B'}}^{c}(A \cap B) = \mathrm{proj}_{X_{B'}}^{c}(A \cap B)$, which means that it follows that the right side of the implication in (11) holds, i.e., $B' \cap (A \cap B) \in \mathcal{G}$. Since A characterizes an arbitrary behavior in $\mathcal{A}$, in accordance with (3), $B' \cap B$ satisfies $(\mathcal{A}, \mathcal{G})$. Since B characterizes an arbitrary behavior $B \in \mathcal{I}_X$ satisfying $(\mathcal{A}, \mathcal{G})$, it follows that $\forall B \in \mathcal{I}_X$. B satisfies $(\mathcal{A}, \mathcal{G}) \Rightarrow B' \cap B$ satisfies $(\mathcal{A}, \mathcal{G})$, which ends the proof. $\square$

**Example 9.** Consider contract $(\mathcal{A}, \mathcal{G})$ and behavior $B'$ from Example 8. As previously mentioned, it holds that: i) $B' \in \mathcal{I}_{\{u,v\}}$; ii) $\mathcal{G}$ is agnostic to $\{u, v, y\} \supseteq \{u, v\}$ and $\emptyset \notin \mathcal{G}$; and iii) $\mathcal{A} \subseteq \mathcal{I}_{\{u,v\}^c}$. In accordance with Theorem 2, to establish that the composition of $B'$ and a behavior B satisfies contract $(\mathcal{A}, \mathcal{G})$, it suffices to show that B satisfies $(\mathcal{A}, \mathcal{G})$ and implements an interface specification for a subset of $\{x, y\}$. An example of such a behavior is $B = \{(x, y, u, v) \in \Omega | x = y\}$, presented in Example 8. $\square$

# 5 Conclusion

As argued for, and exemplified in Section 1, to support properties that may be invalidated through composition, a contracts theory should not have composition inherently monotonic with respect to implementation. Therefore, the paper has presented, as a first contribution, the basis for a novel contracts theory where composition is non-monotonic with respect to implementation. The key solution is that specifications are represented as sets of sets of runs instead of only sets of runs as in previous theories.

The general support from non-monotony implies that cases where monotony is indeed desired needs to be managed explicitly. To support this, the paper has, as a second contribution, presented Corollary 1 and Theorem 1 and 2, which each provides conditions to ensure monotony of composition with respect to implementation when indeed desired.

# References

1. Bauer, S., David, A., Hennicker, R., Guldstrand Larsen, K., Legay, A., Nyman, U., WÄ...sowski, A.: Moving from Specifications to Contracts in Component-Based
Design. In: Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Eng., Lec. Notes in Computer Science, vol. 7212, pp. 43–58. Springer Berlin Heidelberg (2012), http://dx.doi.org/10.1007/978-3-642-28872-2\$_3

2. Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple Viewpoint Contract-Based Specification and Design. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.P. (eds.) Formal Methods for Components and Object, pp. 200–225. Springer-Verlag, Berlin, Heidelberg (2008), http://dx.doi.org/1multiviewPoint0.1007/978-3-540-92188-2\_9

3. Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T., Larsen, K.G.: Contracts for System Design. Rapport de recherche RR-8147, INRIA (Nov 2012), http://hal.inria.fr/hal-00757488

4. Benveniste, A., Caillaud, B., Passerone, R.: Multi-Viewpoint State Machines for Rich Component Models. In: Nicolescu, G., Mosterman, P. (eds.) Model-Based Design for Embedded Systems, pp. 487–518. Taylor & Francis (2009), http://www.google.se/books?id=8Cjg2mM-m1MC

5. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A Theory of Communicating Sequential Processes. J. ACM 31(3), 560–599 (Jun 1984), http://doi.acm.org/10.1145/828.833

6. Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: 2012 38th Euromicro Conference on Software Engineering and Advanced Applications. pp. 21–28 (Sept 2012)

7. Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. In: Proceedings of the fifth MIT conference on Advanced research in VLSI. pp. 51–65. MIT Press, Cambridge, MA, USA (1988), http://dl.acm.org/citation.cfm?id=88056.88061

8. Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Commun. ACM 12(10), 576–580 (Oct 1969), http://doi.acm.org/10.1145/363235.363259

9. Maier, P.: A Set-Theoretic Framework for Assume-Guarantee Reasoning. In: Orejas, F., Spirakis, P., van Leeuwen, J. (eds.) Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 2076, pp. 821–834. Springer Berlin Heidelberg (2001), http://dx.doi.org/10.1007/3-540-48224-5\_67

10. Meyer, B.: Applying "Design by Contract". IEEE Computer 25, 40–51 (1992)

11. Negulescu, R.: Process Spaces. In: Proceedings of the 11th Int. Conf. on Concurrency Theory. pp. 199–213. CONCUR '00, Springer-Verlag, London, UK, UK (2000), http://dl.acm.org/citation.cfm?id=646735.701627

12. Quinton, S., Graf, S.: Contract-based verification of hierarchical systems of components. In: Software Engineering and Formal Methods, 2008. SEFM '08. Sixth IEEE International Conference on. pp. 377–381 (nov 2008)

13. Westman, J., Nyberg, M.: Conditions of contracts for separating responsibilities in heterogeneous systems. Formal Methods in System Design (Sep 2017), https://doi.org/10.1007/s10703-017-0294-7

14. Wolf, E.S.: Hierarchical Models of Synchronous Circuits for Formal Verification and Substitution. Ph.D. thesis, Stanford University, Stanford, CA, USA (1996), uMI Order No. GAX96-12052
A Propositions and Lemmas

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

**Lemma 2.** For any two sets of variables X and Y, it holds that

$$
\mathrm{proj}_Y(\mathrm{proj}_X \mathbf{B}) = \mathrm{proj}_{X \cap Y} \mathbf{B} .
$$

Proof. Consider an arbitrary ω ∈ proj<sub>Y</sub>(proj<sub>X</sub> B). In accordance with Definition 3, this means that ∃μ . ω[Y] = μ[Y] ∧ μ ∈ {ω' ∈ Ω|ω'[X] = ν[X], ν ∈ B}. This can be rewritten as ∃ν∃μ . ω[Y] = μ[Y] ∧ μ[X] = ν[X] ∧ ν ∈ B. Since X ∩ Y ⊆ X and X ∩ Y ⊆ Y, and μ[X] = ν[X] and ω[Y] = μ[Y], it holds that μ[X ∩ Y] = ν[X ∩ Y] and ω[X ∩ Y] = μ[X ∩ Y], which also means that ω[X ∩ Y] = ν[X ∩ Y]. Thus, it holds ∃ν∃μ . ω[X ∩ Y] = ν[X ∩ Y] ∧ ν ∈ B. In accordance with Definition 3, this means that ω ∈ proj<sub>X∩Y</sub> B. Since ω represents an arbitrary run in proj<sub>Y</sub>(proj<sub>X</sub> B), it must hold that each run in proj<sub>Y</sub>(proj<sub>X</sub> B) is also in proj<sub>X∩Y</sub> B, which means that proj<sub>Y</sub>(proj<sub>X</sub> B) ⊆ proj<sub>X∩Y</sub> B.

Next consider an arbitrary ω ∈ proj<sub>X∩Y</sub> B. In accordance with Definition 3,
this means that ∃ν . ω[X ∩ Y] = ν[X ∩ Y] ∧ ν ∈ B. Create a run μ such that
μ[X] = ν[X] and μ[X<sup>C</sup>] = ω[X<sup>C</sup>]. Since μ[X<sup>C</sup>] = ω[X<sup>C</sup>], ω[X ∩ Y] = ν[X ∩ Y],
and Y ⊆ X<sup>C</sup> ∪ (X ∩ Y), it follows that ω[Y] = μ[Y]. Thus, we have shown that
∃ν∃μ . ω[Y] = μ[Y] ∧ μ[X] = ν[X] ∧ ν ∈ B, which can, as previously mentioned, be
rewritten as ∃μ . ω[Y] = μ[Y] ∧ μ ∈ {ω' ∈ Ω|ω'[X] = ν[X], ν ∈ B}. In accordance
with Definition 3, this means that ω ∈ proj<sub>Y</sub>(proj<sub>X</sub> B). Since ω represents an
arbitrary run in proj<sub>X∩Y</sub> B, it must hold that each run in proj<sub>X∩Y</sub> B is also
in proj<sub>Y</sub>(proj<sub>X</sub> B), which means that proj<sub>X∩Y</sub> B ⊆ proj<sub>Y</sub>(proj<sub>X</sub> B). Since it
was previously also shown that proj<sub>Y</sub>(proj<sub>X</sub> B) ⊆ proj<sub>X∩Y</sub> B, it follows that
proj<sub>Y</sub>(proj<sub>X</sub> B) = proj<sub>X∩Y</sub> B, which ends the proof.
□

**Lemma 3.** It holds that $\mathrm{proj}_{X_B} \mathbf{B} = \mathbf{B}$.

Proof. In accordance with Definition 4, it holds that $\mathrm{proj}_{\{x\}}^c \mathbf{B} = \mathbf{B}$ for each variable in $X_{\mathbf{B}}^c = \{x_1, \dots, x_N\}$. It follows that

$$
\mathrm{proj}_{\{x_1\}}(\mathrm{proj}_{\{x_2\}}(\dots\mathrm{proj}_{\{x_N\}}(\mathbf{B})\dots)) = \mathbf{B}.
$$

It follows in accordance with Lemma 2 that $\mathrm{proj}_{\{x_1\}}^c \cap \dots \cap \{x_N\}}^c \mathbf{B} = \mathbf{B}$ and since
$X_{\mathbf{B}} = \{x_1\}^c \cap \dots \cap \{x_N\}^c$, it also holds that $\mathrm{proj}_{X_{\mathbf{B}}} \mathbf{B} = \mathbf{B}$, which ends the
proof.
$\square$

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

$$
\mathrm{proj}_Y(\mathbf{B}_1 \cap \mathbf{B}_2) = \mathrm{proj}_Y \mathbf{B}_1 \cap \mathrm{proj}_Y \mathbf{B}_2 .
$$

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

To prove also that $\text{proj}_Y B_1 \cap \text{proj}_Y B_2 \subseteq \text{proj}_Y(B_1 \cap B_2)$, consider an arbitrary run $\omega \in \text{proj}_Y B_1 \cap \text{proj}_Y B_2$. According to Definition 3 this means that:

$$ \exists \nu_1 \in B_1. \nu_1[Y] = \omega[Y] $$

$$ \exists \nu_2 \in B_2. \nu_2[Y] = \omega[Y] $$

Now consider the vector $\nu = (\nu_1[X_{B_1}], \nu_2[X_{B_2}])$. Clearly it holds that $\omega[Y] = \nu[Y]$.

Since $\nu_1 \in B_1$, and $\nu[X_{B_1}] = \nu_1[X_{B_1}]$, it holds according to Definition 3 that $\nu \in \text{proj}_{X_{B_1}} B_1$. Then, according to Lemma 3, it also holds that $\nu_1 \in B_1$. Similarly, since $\nu_2 \in B_2$, and $\nu[X_{B_2}] = \nu_2[X_{B_2}]$, it must hold that $\nu \in B_2$.

Thus, we have shown that $\nu \in B_1 \cap B_2$ and that $\omega[Y] = \nu[Y]$. Therefore, according to Definition 3, it holds that $\omega \in \text{proj}_Y(B_1 \cap B_2)$, which ends the proof. $\square$

**Proposition 2.** It holds that $\text{proj}_Y B = \Omega$ if $Y \cap X_B \neq \emptyset$.

*Proof.* In accordance with Lemma 3, it holds that $\text{proj}_Y B = \text{proj}_Y(\text{proj}_{X_B} B)$, and further that $\text{proj}_Y B = \text{proj}_{Y \cap X_B} B$ in accordance with Lemma 2. If $Y \cap X_B \neq \emptyset$, it follows that $\text{proj}_Y B = \text{proj}_{\emptyset} B = \Omega$. $\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 $B \in \mathcal{Q}$ and a $B'$ such that $\text{proj}_{Y \cap C} B' = \text{proj}_{Y \cap C} B$. Since $X^C \subseteq Y^C$, it holds according to Lemma 2, that

$$ \text{proj}_{X^C} B' = \text{proj}_{X^C} \text{proj}_{Y \cap C} B' = \text{proj}_{X^C} \text{proj}_{Y \cap C} B = \text{proj}_{X^C} B $$

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

**Lemma 5.** Given two behaviors $B$ and $B'$ where $B \cap B' \neq \emptyset$, it holds that $X_{B \cap B'} \subseteq X_B \cup X_{B'}$.

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

$$ B = \text{proj}_{\{x\}C} B, \qquad (12) $$

$$ B' = \text{proj}_{\{x\}C} B', \text{ and} \qquad (13) $$

$$ B \cap B' \neq \text{proj}_{\{x\}C}(B \cap B'). \qquad (14) $$

Proposition 1 and (14) imply $B \cap B' \neq \text{proj}_{\{x\}C} B \cap \text{proj}_{\{x\}C} B'$, which in combination with (12) and (13) imply that $B \cap B' \neq B \cap B'$. Since this is a contradiction, assumption $X_{B \cap B'} \not\subseteq X_B \cup X_{B'}$ must be false, and it must rather hold that $X_{B \cap B'} \subseteq X_B \cup X_{B'}$, which completes the proof. $\square$