# Some Algebraic Aspects of Assume-Guarantee Reasoning

Inigo Incer, Albert Benveniste, Alberto Sangiovanni-Vincentelli

► To cite this version:

Inigo Incer, Albert Benveniste, Alberto Sangiovanni-Vincentelli. Some Algebraic Aspects of Assume-Guarantee Reasoning. 2024. [hal-04807237](https://hal.science/hal-04807237v1)

HAL Id: hal-04807237

https://hal.science/hal-04807237v1

Preprint submitted on 27 Nov 2024

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
# Some Algebraic Aspects of Assume-Guarantee Reasoning*

Inigo Incer¹, Albert Benveniste², and Alberto Sangiovanni-Vincentelli³

¹ California Institute of Technology, Pasadena, CA, USA

² INRIA/IRISA, Rennes, France

³ University of California, Berkeley, CA, USA

**Abstract.** We present the algebra of assume-guarantee (AG) contracts. We define contracts, provide new as well as known operations, and show how these operations are related. Contracts are functorial: any Boolean algebra has an associated contract algebra. We study monoid and semiring structures in contract algebra—and the mappings between such structures. We discuss the actions of a Boolean algebra on its contract algebra.

## 1 Introduction

The design of complex cyber-physical systems (CPS) involves fundamental challenges in modeling, specification, and integration. Among the modeling challenges, the need to model the interconnection of components modeled using discrete transitions with those using differential equations is fundamental. It is the opposition between the discrete and the continuous, which René Thom calls “the fundamental aporia of mathematics.” Specification is well known to be hard in system engineering: practitioners consistently rank the generation of specifications for a project among the top challenges in system design [23, 27]. Finally, integration has seen steep increases in magnitude in the 20th century, bringing technical challenges to engineering (how do we design, build, and maintain such systems?)<fnref n="4" /> and organizational challenges to the business landscape (how does an organization change to support the development, construction, and maintenance of such systems?)<fnref n="5" />. The organizational challenges of system engineering are so salient that some authors categorize the field as a branch of management [7, 17].

<footnote>* This paper is based on Chapter 6 of [14].</footnote>

<footnote n="4">⁴ We read, for example: “We are increasingly experiencing a new type of accident that arises in the interactions among components (electromechanical, digital, and human) rather than in the failure of individual components” [19]. “Almost all SI [system integration] failures occur at interfaces primarily due to incomplete, inconsistent, or misunderstood specifications” [20].</footnote>

<footnote n="5">⁵ Hobday et al. [11] argue that “systems integration has evolved beyond its original technical and operational tasks to encompass a strategic business dimension becoming, therefore, a core capability of many high-technology corporations. . . The more complex, high-technology, and high cost the product, the more significant systems integration becomes to the productive activity of the firm. . . Systems integration capabilities are inextricably linked to decisions on whether to make in-house, out-</footnote>
Werner Damm has championed two key concepts to address system design challenges: rich components and contracts. In [5], he observes that “the design of components in complex systems inherently involves multi-site, multi-domain and cross-organizational design teams” and that “in spite of well-defined and enforced process models, such as the V-model, a multitude of ‘disturbances’ may lead to undesirable design iterations. ‘Disturbances’ in this context take a variety of forms, such as late or incomplete sets of requirements, late requirement changes, unspecified assumptions, unexpected disruption in a supply chain sub-process, the failure to meet non-functional constraints such as communication latencies, implicit interdependencies, etc.” One way to deal with these disturbances is by characterizing the domains of validity of our models. In [5], a rich component is proposed as a classical component upgraded by

(1) extending component specifications to cover all viewpoints necessary for electronic system design; (2) explicating the dependency of such specifications on assumptions on the context of a component; (3) providing classifiers to such assumptions, relating both the positioning in a layered design space (horizontal, up, down), as well as to their confidence level.

The idea of representing components using assume-guarantee (AG) contracts launched a major research effort in system engineering [3, 4, 12, 25, 28]. We wanted to streamline two key aspects of complex system design: relationships between a system integrator and its suppliers (cross-organizational design) and the interactions between multiple engineering organizations within the same company (cross-domain design). In contract-based design, to each component in our system we assign an assume-guarantee specification—or contract. A rich contract algebra [4,14] allows us to relate global system properties to the local properties of the components it comprises. This algebra provides mathematical support for key aspects of the system design process. In this paper, we present this algebra and discuss its role in system design.

**Contracts.** AG contracts can be understood as formal specifications split in two parts: (i) assumptions made on the environment, and (ii) responsibilities assigned to the object satisfying the specification when it is instantiated in an environment which meets the assumptions of the contract. Contracts were introduced to streamline the integration of complex systems and to support concurrent design. System integration pertains to the composition of multiple design objects into a coherent whole. For example, suppose a company wishes to implement a system with a specification *C*; designers may realize that there are two sub-specifications *C*₁ and *C*₂ such that the composition of their implementations always yields an implementation for the top level specification. In the language of AG contracts, we would say that the composition of *C*₁ and *C*₂, written *C*₁ || *C*₂, *refines* *C*. This company may now develop an implementation *M*₁ for *C*₁, and assign *C*₂ to a

<footnote>source, or collaborate in production and competition.” Davies et al. [6] claim that “the traditional advantages of the vertically-integrated systems seller offering single-vendor designed systems is no longer a major source of competitive advantage in many industries.”</footnote>
third-party OEM to deliver an implementation $M_2$. If $M_2$ is an implementation for $C_2$, the original company knows that $M_1$ and $M_2$ can be composed and that this composition meets the top-level specification $C$. In this setting, frictions in the supply chain are alleviated as companies exchange formal specifications expressed as contracts.

An additional use of contracts is as follows. Suppose our company wants to implement a system with a specification $C$ using a component $M_1$ with specification $C_1$ that is not sufficient to implement $C$. Contracts provide an operation called *quotient* which yields the specification whose implementation is *exactly* the component $M'$ such that $M_1$ composed with $M'$ meets the specification $C$. The operation of quotient has uses in synthesis (when we have made incremental progress towards meeting a goal) and in every situation where we need to find *missing components*.

To say that contracts support concurrent design refers to another aspect of the design process. The design of some components involves multiple engineers working on different aspects of the same object. For example, a team may work on the functionality aspects of an integrated circuit, while another works on its timing characterization. If the functionality team generates a specification $C_f$, and the timing team generates a specification $C_t$, the two teams can combine their specs into a single contract object $C$ through an operation called *merging*. In contract theory, these various aspects of a component are called *viewpoints*.

The work on the assume-guarantee reasoning of Floyd-Hoare logic [8, 10], on assume-guarantee specifications of Lamport and Abadi [1, 18], on design by contract by Meyer [22], on interface automata by de Alfaro and Henzinger [2], and applications of formal specifications to cyber-physical systems by Damm [5], yielded that formal assume-guarantee specifications could be used to design and analyze any cyber-physical system, including their discrete and continuous aspects. Assume-guarantee contracts were thus introduced for this purpose by Benveniste et al. in [3]. Cyber-physical-system design methodologies using contracts were described in [25, 29].

Two questions of practical relevance (the related discussions are written in blue) inform our discussion below. *Question 1: how can multiple specifications be combined to generate a system specification?* This leads us to consider binary operations on assume-guarantee contracts and their uses in the system design process. The question has a corollary: *when a system is decomposed across multiple suppliers, as well as across multiple viewpoints, is there a right order for applying the contract operations? Does the result depend on this order?* This question will lead us to consider how the various operations interact among themselves.

The second question has to do with computational complexity. We know that abstracting specifications tends to yield computationally-friendlier semidecision procedures. *Question 2: how can we compute contract abstractions?* Part of our answer to this question will make use of semiring actions.

The structure of the paper is as follows. Section 2 begins to address Question 1 by covering the standard definitions of contracts [4] and all known contract
operations. The content of this section is a review, except for the operations of implication and coimplication, which, to the best of our knowledge, have not been published before. Section 3 treats contracts as an algebra associated with any Boolean algebra and presents a study of monoid and semiring structures within a contract algebra. In other words, this section deals with how the various contract operations interact with each other, yielding insight into compositional design methodologies using contracts. We use these results to define contract actions, which play a role in answering Question 2. Section 4 covers two ways in which a Boolean algebra can act on its contract algebra, and Section 5 discusses contract abstractions. Sections 3-5 summarize the contributions of this paper.

## 2 Assume-guarantee contracts

This section defines assume guarantee contracts and addresses Question 1: how can multiple specifications be combined to generate a system specification?

We discuss four binary operations that allow us to combine contracts. We also explore adjoint operations that allow us to carry out contract decompositions optimally. The content in this section borrows from [4, 24], and the references in the text. Its contributions are the closed-form expressions for implication and coimplication and the use of duality to unify the presentation of the contract operations.

Let $\mathcal{B}$ be a set called the *universe of behaviors*. Its elements are called *behaviors*. The universe of behaviors fixes the modeling formalism we have chosen in our application. A property is defined as a subset of $\mathcal{B}$. A component is also a subset of $\mathcal{B}$. The difference is semantics: we think of components as the set of behaviors they can display. Properties contain behaviors meeting a certain criterion. We say that a component $M$ satisfies a property $P$, written $M \models P$ if $M \subseteq P$. Assume-guarantee contracts are pairs of properties.

**Definition 1.** A contract $C$ is a pair of properties $C = (A, G)$. We call $A$ assumptions, and $G$ guarantees.

Components can have two types of relationships with respect to a contract.

**Definition 2.** Let $C = (A, G)$ be a contract. We say that a component $E$ is an environment for $C$, written $E \models^E C$, if $E \models A$.

Environments are those components which meet the assumptions of a contract. Implementations are those which meet the guarantees of the contract when operating in an environment accepted by the contract.

**Definition 3.** Let $C = (A, G)$ be a contract. We say that a component $M$ is an implementation for $C$, written $M \models^M C$, if $M \parallel E \models G$ for every environment $E$ of $C$.

Now that we have definitions for environments and implementations, we define a relation on contracts that declares two contracts equivalent when they have the same environments and the same implementations:
**Definition 4.** Let $\mathcal{C}$ and $\mathcal{C}'$ be two contracts. We say they are equivalent when they have the same environments and the same implementations.

This means that for $\mathcal{C} = (A, G)$ and $\mathcal{C}' = (A', G')$ to be equivalent, we must have $A = A'$ and $G \cap A = G' \cap A' = G' \cap A$ (because $A' = A$). The largest $G'$ meeting this condition is $G' = G \cup \neg A$ (the complement is taken with respect to $\mathcal{B}$). Enforcing this constraint for a contract allows us to have a unique mathematical object for each set of environments and implementations. We thus define an AG contract in canonical form as follows:

**Definition 5.** A contract in canonical form is a contract $\mathcal{C} = (A, G)$ satisfying $A \cup G = \mathcal{B}$.

From now on, we assume all contracts are in canonical form.

**2.1 Duality**

There is a unary operation which is helpful in revealing structure for AG contracts.

**Definition 6.** Let $\mathcal{C} = (A, G)$ be a contract. We define a unary operation called reciprocal as follows: $\mathcal{C}^{-1} = (G, A)$.

This operation flips environments and implementations, i.e., it gives us the “environment view” of the specification $\mathcal{C}$. Note that the reciprocal respects canonicity.

**Definition 7.** Let $\circ$ and $\star$ be two binary operations on AG contracts, we say that the operations are dual when $(C_a \circ C_b)^{-1} = C_a^{-1} \star C_b^{-1}$.

**2.2 Order**

**Definition 8.** Suppose $\mathcal{C}$ and $\mathcal{C}'$ are two contracts. We say that $\mathcal{C}$ is a refinement of $\mathcal{C}'$, written $\mathcal{C} \le \mathcal{C}'$, when all implementations of $\mathcal{C}$ are implementations of $\mathcal{C}'$ and all environments of $\mathcal{C}'$ are environments of $\mathcal{C}$.

The association we make of a specification being a refinement is that it is harder to meet than another. This is why we say that a specification accepting more environments is a refinement of one accepting less. We can express this order relation using assumptions and guarantees.

**Proposition 1 (Theorem 5.2 of [4]).** Let $\mathcal{C} = (A, G)$ and $\mathcal{C}' = (A', G')$ be two contracts. Then $\mathcal{C} \le \mathcal{C}'$ when $G \subseteq G'$ and $A' \subseteq A$.
## 2.3 Conjunction and disjunction

The notion of order provides a lattice structure to AG contracts in canonical form. Given contracts $C = (A, G)$ and $C' = (A', G')$, their meet (GLB) and join (LUB) are given by

$$C \wedge C' = (A \cup A', G \cap G') \quad \text{and} \quad C \vee C' = (A \cap A', G \cup G').$$

We leave it to the reader to verify that conjunction and disjunction are monotonic with respect to the refinement order. Also, conjunction and disjunction furnish our first example of dual operations: $C \wedge C' = (G \cap G', A \cup A')^{-1} = ((G, A) \vee (G', A'))^{-1} = (C^{-1} \vee C'^{-1})^{-1}$.

If we interpret a contract as the entailment $A \Rightarrow G$, then contract conjunction is the conjunction of such entailments. Conjunction can be used to combine viewpoints. Disjunction has an application in product lines.

## 2.4 Composition

The notion of composition of AG contracts yields the specification of systems obtained from composing implementations of each of the contracts being composed. Contract composition formalizes how contracts with suppliers result in a system level contract. This operation is defined by axiom as follows:

Suppose $C_1$ and $C_2$ are two specifications to be composed. Call $C$ the composite specification. Let $M_1$ and $M_2$ be arbitrary implementations of $C_1$ and $C_2$, respectively, and let $E$ be any environment of $C$. We define $C$ to be the smallest contract satisfying the following constraints: the composite $M_1 \parallel M_2$ is an implementation of $C$; the composite $M_1 \parallel E$ is an environment of $C_2$; and the composite $M_2 \parallel E$ is an environment of $C_1$.

The first requirement states that composing implementations of the specs being composed yields an implementation of the composite specification. The second requirement states that instantiating an implementation of $C_1$ in an environment of the composite specification yields an environment for $C_2$. And the last requirement is the analogous statement for $C_1$. This principle, which states how to compose specifications split between environment and implementation requirements, was stated for the first time by M. Abadi and L. Lamport [1]. We can obtain a closed-form expression of this principle for AG contracts:

**Proposition 2 (Theorem 5.2 of [4]).** Let $C_1 = (A_1, G_1)$ and $C_2 = (A_2, G_2)$ be two AG contracts. Their composition, denoted $C_1 \parallel C_2$, is given by $C_1 \parallel C_2 = (A_1 \cap A_2 \cup \neg(G_1 \cap G_2), G_1 \cap G_2)$.

We state without proof an important property of composition:

**Proposition 3.** *Composition of AG contracts is monotonic with respect to the refinement order.*
## 2.5 Strong merging (or merging)

We said that AG contracts are used to handle the specifications of the various viewpoints of the same design element. Suppose $C_1$ and $C_2$ are specifications corresponding to different aspects to the same design object, e.g., functionality and power. We define their merger, denoted $C_1 \bullet C_2$, to be the contract which guarantees the guarantees of both specifications when the assumptions of both specifications are respected: $C_1 \bullet C_2 = (A_1 \cap A_2, G_1 \cap G_2 \cup \neg(A_1 \cap A_2))$. This contract is equivalent to contract $(A_1 \cap A_2, G_1 \cap G_2)$, which is exactly what we defined merging to be. Merging can be used to combine viewpoints. Merging and composition are duals, as pointed out in [24].

## 2.6 Adjoints

We have introduced four operations on AG contracts: two were obtained from the partial order, and two by axiom. Now we obtain the adjoints of these operations. Adjoints are used to compute optimal decompositions of contracts.

**Quotient (or residual)** The adjoint of composition is called quotient. Let $C$ and $C'$ be two AG contracts. The quotient (also called residual in the literature), denoted $C/C'$, is defined as the largest AG contract $C''$ satisfying $C' \parallel C'' \leq C$.

Due to the fact that the quotient is the largest contract with this property, Proposition 3 tells us that any of its refinements has this property.

If we interpret $C$ as a top-level specification that our system has to meet (e.g., the specification of a vehicle), and $C'$ as the specification of a subset of the design for which we already have an implementation (e.g., a powertrain), then the quotient is the specification whose implementations are exactly those components that, if added to our partial design, would yield a system meeting the top-level specification. The following proposition gives us a closed-form expression for the quotient of AG contracts:

**Proposition 4 (Theorem 3.5 of [13])** Let $C = (A, G)$ and $C' = (A', G')$ be two AG contracts. The quotient, denoted $C/C'$, is given by

$$C/C' = (A \cap G', G \cap A' \cup \neg(A \cap G')).$$

For an in-depth study of the notion of a quotient across several compositional theories, see [16]. We can readily show that

$$C/C' = C \bullet (C')^{-1}. \qquad (1)$$

**Separation** Just like composition has an adjoint operation (the quotient), merging has an adjoint. For contracts $C$ and $C'$, we define the operation of separation, denoted $C \div C'$, as the smallest contract $C''$ satisfying $C \leq C' \bullet C''$. This operation has a closed-form solution:
**Proposition 5 (Theorem 3.12 of [26]).** Let $C = (A, G)$ and $C' = (A', G')$ be two AG contracts. Then $C \div C' = (A \cap G' \cup \neg(G \cap A'), G \cap A')$.

Separation obeys $C \div C' = C \parallel (C')^{-1}$. From this identity and (1), it follows that quotient and separation are duals. For examples of merging and separation, see [26].

**Implication and coimplication** Given contracts $C$ and $C'$, the definition of implication, denoted $C' \to C$, in a lattice is $\forall C''. C'' \wedge C' \le C \Leftrightarrow C'' \le (C' \to C)$. In other words, $C' \to C$ is the largest contract $C''$ satisfying $C'' \wedge C' \le C$. The following proposition tells us how to compute this object:

**Proposition 6.** Let $C = (A, G)$ and $C' = (A', G')$ be two contracts. Implication has the closed form expression $C' \to C = ((A \cap \neg A') \cup (G' \cap \neg G), G \cup \neg G')$.

Dually, we can ask what is the smallest contract $C''$ satisfying $C'' \vee C' \ge C$. We will denote this object $C' \to C$. A similar proof yields the following proposition.

**Proposition 7.** Let $C = (A, G)$ and $C' = (A', G')$ be two contracts. The smallest contract $C''$ satisfying $C'' \vee C' \ge C$ has the closed form expression $C' \to C = (A \cup \neg A', (G \cap \neg G') \cup (A' \cap \neg A))$.

We observe that

$$C' \to C = (G \cup \neg G', (A \cap \neg A') \cup (G' \cap \neg G))^{-1} = ((C')^{-1} \to C^{-1})^{-1},$$

which shows that implication and coimplication are duals.

## 2.7 Summary of binary operations

The following diagram shows how all AG contract operations are related.

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

Two operations—conjunction and disjunction—come from the definition of order, and two—composition and merging—are defined by axiom. The rest of the operations are adjoints of these four.

# 3 Algebraic structures within contracts

In this section, we investigate the corollary of Question 1: Since both viewpoints and subsystems specifications need to be combined, does the order among these operations influence the result? If yes, is there a best order?

Inspection of the various binary formulas for AG contracts suggests that contracts can be defined over any Boolean algebra, not just that corresponding to properties over a set of behaviors. From now on, we deal with contracts defined
<table><caption>Table 1: Closed-form expressions of operations for contracts over a Boolean algebra</caption><thead><tr><th>Conjunction</th><th>Disjunction</th></tr></thead><tbody><tr><td>C ∧ C' = (a ∨ a', g ∧ g')</td><td>C ∨ C' = (a ∧ a', g ∨ g')</td></tr><tr><td>Composition</td><td>Merging</td></tr><tr><td>C<sub>1</sub> || C<sub>2</sub> = (a<sub>1</sub> ∧ a<sub>2</sub> ∨ ¬(g<sub>1</sub> ∧ g<sub>2</sub>), g<sub>1</sub> ∧ g<sub>2</sub>)</td><td>C<sub>1</sub> • C<sub>2</sub> = (a<sub>1</sub> ∧ a<sub>2</sub>, g<sub>1</sub> ∧ g<sub>2</sub> ∨ ¬(a<sub>1</sub> ∧ a<sub>2</sub>))</td></tr><tr><td>Quotient</td><td>Separation</td></tr><tr><td>C/C' = (a ∧ g', g ∧ a' ∨ ¬(a ∧ g'))</td><td>C ÷ C' = (a ∧ g' ∨ ¬(g ∧ a'), g ∧ a')</td></tr><tr><td>Implication</td><td>Coimplication</td></tr><tr><td>C' → C = ((a ∧ ¬a') ∨ (g' ∧ ¬g), g ∨ ¬g')</td><td>C' → C = (a ∨ ¬a', (g ∧ ¬g') ∨ (a' ∧ ¬a))</td></tr></tbody></table>

over an arbitrary Boolean algebra and embark on a study of the relations between the various contract operations.

Let $B$ be a Boolean algebra with bottom and top elements $0_B$ and $1_B$, respectively. We form the contract algebra $C(B)$ associated with $B$. The elements of $C(B)$ are all pairs $(a, b) \in B^2$ such that $a \lor b = 1_B$. The notions of order and the binary operations work exactly the same as for AG contracts over sets of behaviors. Table 1 summarizes these operations.

The contract $1 = (0_B, 1_B)$ is larger than any contract. $0 = (1_B, 0_B)$ is smaller than any contract. The contract $e = (1_B, 1_B)$ is an identity for composition and merging. $1$ is an identity for conjunction, and $0$ for disjunction. Table 2 shows how various operations behave with respect to the distinguished elements.

<table><caption>Table 2: Contract operations and the distinguished elements</caption><thead><tr><th>0</th><th>1</th><th>e</th></tr></thead><tbody><tr><td>C ∧ 0 = 0</td><td>C ∧ 1 = C</td><td>(a, g) ∧ e = (1<sub>B</sub>, g)</td></tr><tr><td>C ∨ 0 = C</td><td>C ∨ 1 = 1</td><td>(a, g) ∨ e = (a, 1<sub>B</sub>)</td></tr><tr><td>C || 0 = 0</td><td>(a, g) || 1 = (¬g, g)</td><td>C || e = C</td></tr><tr><td>(a, g) • 0 = (a, ¬a)</td><td>C • 1 = 1</td><td>C • e = C</td></tr><tr><td>C/0 = 1</td><td>(a, g)/1 = (a, ¬a)</td><td>C/e = C</td></tr><tr><td>0/(a, g) = (g, ¬g)</td><td>1/C = 1</td><td>e/C = C<sup>-1</sup></td></tr><tr><td>(a, g) ÷ 0 = (¬g, g)</td><td>C ÷ 1 = 0</td><td>C ÷ e = C</td></tr><tr><td>0 ÷ C = 0</td><td>1 ÷ (a, g) = (¬a, a)</td><td>e ÷ C = C<sup>-1</sup></td></tr><tr><td>(a, g) → 0 = (g, ¬g)</td><td>C → 1 = 1</td><td>(a, g) → e = (¬a, 1<sub>B</sub>)</td></tr><tr><td>0 → C = 1</td><td>1 → C = C</td><td>e → (a, g) = (¬g, g)</td></tr><tr><td>C → 0 = 0</td><td>(a, g) → 1 = (¬a, a)</td><td>(a, g) → e = (1<sub>B</sub>, ¬g)</td></tr><tr><td>0 → C = C</td><td>1 → C = 0</td><td>e → (a, g) = (a, ¬a)</td></tr></tbody></table>

## 3.1 Monoids

We begin to study the interactions among the various operations. We recall that a monoid is a semigroup with identity, i.e., a set together with an associative
binary operation and an identity element for that operation. A contract algebra contains several monoids:

**Proposition 8.** $C_{\wedge}^{M}(B) = (C(B), \wedge, 1_{B})$, $C_{\vee}^{M}(B) = (C(B), \vee, 0_{B})$, $C_{\parallel}^{M}(B) = (C(B), \parallel, e)$, and $C_{\bullet}^{M}(B) = (C(B), \bullet, e)$ are idempotent, commutative monoids.

It turns out these monoids are isomorphic:

**Proposition 9.** The monoids $C_{\wedge}^{M}(B)$, $C_{\vee}^{M}(B)$, $C_{\parallel}^{M}(B)$, and $C_{\bullet}^{M}(B)$ are isomorphic. Moreover, the following diagram commutes, where $\theta_{g}(a, g) = (\neg(a \wedge g), g)$ and $\theta_{a}(a, g) = (a, \neg(a \wedge g))$:

$$ \begin{array}{ccc} \begin{array}{c} C_{\wedge}^{M}(B) \\ \theta_{g} \uparrow \downarrow \rlap{\scriptstyle{\cdot}} \end{array} & \stackrel{(\cdot)^{-1}}{\rightleftharpoons} & \begin{array}{c} C_{\vee}^{M}(B) \\ \rlap{\scriptstyle{\cdot}} \downarrow \end{array} \\ \begin{array}{c} C_{\parallel}^{M}(B) \end{array} & \stackrel{(\cdot)^{-1}}{\rightleftharpoons} & \begin{array}{c} C_{\bullet}^{M}(B) \end{array} \end{array} \qquad (2) $$

## 3.2 Maps between monoids

The previous result showed how to express contract operations in terms of others. Now we explore how to map contract monoids across their underlying Boolean algebras.

Suppose we have two Boolean algebras, $B$ and $B'$. Due to Proposition 9, it is sufficient to study the structure of the maps between the contract monoids $C_{\parallel}^{M}(B)$ and $C_{\parallel}^{M}(B')$ in order to understand the structure of the maps between all contract monoids associated with each Boolean algebra. First we study maps that allow us to construct and split contracts. Then we consider the general maps.

Let $M_{\wedge}(B)$ and $M_{\vee}(B)$ be the monoids $M_{\wedge}(B) = (B, \wedge, 1_{B})$ and $M_{\vee}(B) = (B, \vee, 0_{B})$. We define the two monoid maps

$$ \iota_a : M_{\wedge}(B) \to C_{\parallel}^{M}(B) \quad a \mapsto (a, 1_{B}) $$

$$ \iota_g : M_{\wedge}(B) \to C_{\parallel}^{M}(B) \quad g \mapsto (1_{B}, g). $$

These maps generate an epic monoid map $\pi: M_{\wedge}(B) \times M_{\wedge}(B) \to C_{\parallel}^{M}(B)$ defined as

$$ (a, g) \mapsto \iota_a(a) \parallel \iota_g(g) = (g \to a, g). $$

Similarly, we have monoid maps that allow us to split a contract:

$$ \pi_g : C_{\parallel}^{M}(B) \to M_{\wedge}(B) \quad \pi_g(a, g) = g $$

$$ \pi_a : C_{\wedge}^{M}(B) \to M_{\vee}(B) \quad \pi_a(a, g) = a. $$

We use the monoid isomorphisms (2) to obtain a map $C_{\wedge}^{M}(B) \to M_{\wedge}(B)$ from the last morphism:

$$ \begin{array}{c} \neg \circ \pi_a \circ \theta_g : C_{\parallel}^{M}(B) \to M_{\wedge}(B) \\ (a, g) \mapsto a \wedge g. \end{array} $$
The two maps $C_{\parallel}^{M}(B) \to M_{\wedge}(B)$ yield the monic monoid map

$$ \iota: C_{\parallel}^{M}(B) \to M_{\wedge}(B) \times M_{\wedge}(B) \\ (a, g) \mapsto (a \wedge g, g). $$

This map is left-invertible:

$\pi \circ \iota = e.$

The elementary maps just described enable us to find the general structure between the monoid maps between the parallel monoids corresponding to two Boolean algebras.

**Theorem 1.** Let $f: C_{\parallel}^{M}(B) \to C_{\parallel}^{M}(B')$. Then we can write $f$ as

$$ f = \pi \circ (l_a(ag)l_g(g)r_a(ag)r_g(g), r_a(ag)r_g(g)) \circ \iota, $$

where $l_a, l_g, r_a, r_g: M_{\wedge}(B) \to M_{\wedge}(B')$ are monoid morphisms.

## 3.3 Semirings

Now that we have four isomorphic monoids, we look for additional algebraic structure within the contract algebra, namely, the existence of semirings. This will capture the interactions between algebraic operations. First we study the distributivity of the binary operations. Distributivity and semi-distributivity answer the corollary of Question 1: Does the order between subspecification composition and viewpoint combination matter?

<table><caption>Table 3: Distributivity of contract operations</caption><thead><tr><th></th><th>Conjunction</th><th>Disjunction</th><th>Composition</th><th>Merging</th></tr></thead><tbody><tr><th>Conjunction</th><td>C ∧ (C' ∧ C'') = C ∧ (C' ∨ C'') = C ∧ (C' || C'') = e ∧ (1 • 0) ≠<br>(C ∧ C') ∧ (C ∧ C'') (C ∧ C') ∨ (C ∧ C'') (C ∧ C') || (C ∧ C'') (e ∧ 1) • (e ∧ 0)</td><td></td><td></td><td></td></tr><tr><th>Disjunction</th><td>C ∨ (C' ∧ C'') = C ∨ (C' ∨ C'') = e ∨ (1 || 0) ≠ C ∨ (C' • C'') =<br>(C ∨ C') ∧ (C ∨ C'') (C ∨ C') ∨ (C ∨ C'') (e ∨ 1) || (e ∨ 0) (C ∨ C') • (C ∨ C'')</td><td></td><td></td><td></td></tr><tr><th>Composition</th><td>C || (C' ∧ C'') = C || (C' ∨ C'') = C || (C' || C'') = 1 || (0 • e) ≠<br>(C || C') ∧ (C || C'') (C || C') ∨ (C || C'') (C || C') || (C || C'') (1 || 0) • (1 || e)</td><td></td><td></td><td></td></tr><tr><th>Merging</th><td>C • (C' ∧ C'') = C • (C' ∨ C'') = 0 • (1 || e) ≠ C • (C' • C'') =<br>(C • C') ∧ (C • C'') (C • C') ∨ (C • C'') (0 • 1) || (0 • e) (C • C') • (C • C'')</td><td></td><td></td><td></td></tr></tbody></table>

**Proposition 10.** Table 3 shows whether the binary operations displayed in the rows distribute over the binary operations in the columns.
If we use conjunction to combine viewpoints, then the distributivity of composition over conjunction says that combining viewpoints and composing subSpecifications can be performed at will, in any order. This is wrong if we use merging to combine viewpoints. Nevertheless, the following proposition expresses that, if we use merging to combine viewpoints, it is preferred to combine viewpoints first, and then compose subSpecifications, than the converse.

**Proposition 11.** Let $C_i$ be a contract for $1 \le i \le 4$. We have the following semi-distributions:

$$ (C_1 \wedge C_2) \star (C_3 \wedge C_4) \le (C_1 \star C_3) \wedge (C_2 \star C_4) \quad \text{and} \\ (C_1 \vee C_2) \star (C_3 \vee C_4) \ge (C_1 \star C_3) \vee (C_2 \star C_4), $$

where $\star$ is any of the operations conjunction, disjunction, composition, or merging.

The sub-distributivity of parallel composition over conjunction is proved in Chapter 4 of [4]. We will now use the distributivity results to look for semiring structure within the algebra of contracts. We recall the definition of a semiring (see, e.g., [9]):

**Definition 9.** A semiring $(R, \cdot, +, 1_R, 0_R)$ is a nonempty set $R$ where (a) $(R, +, 0_R)$ is a commutative monoid; (b) $(R, \cdot, +, 1_R)$ is a monoid; (c) $r(s + t) = rs + rt$ and $(s + t)r = sr + tr$ for all $r, s, t \in R$; (d) $r \cdot 0_R = 0_R \cdot r = 0_R$ for all $r \in R$; and (e) $0_R \ne 1_R$.

A map of semirings $f: (R, \cdot, +, 1_R, 0_R) \to (R', \cdot, +, 1_{R'}, 0_{R'})$ satisfies (a) $f(0_R) = f(0_{R'})$, (b) $f(1_R) = f(1_{R'})$, (c) $f(r + s) = f(r) + f(s)$, and (d) $f(r \cdot s) = f(r) \cdot f(s)$.

The following result provides the semiring structures available in the contract algebra.

**Proposition 12.** Using the operations of conjunction, disjunction, composition, and merging, we have exactly four semirings: (a) the conjunction semiring $C_{\wedge}^{S}(B) = (C(B), \wedge, \vee, 1, 0)$, (b) the disjunction semiring $C_{\vee}^{S}(B) = (C(B), \vee, \wedge, 0, 1)$, (c) the composition semiring $C_{\parallel}^{S}(B) = (C(B), \parallel, \vee, e, 0)$, and (d) the merging semiring $C_{\bullet}^{S}(B) = (C(B), \bullet, \wedge, e, 1)$.

These four semirings have two isomorphisms.

**Proposition 13.** We have the isomorphisms $C_{\wedge}^{S}(B) \cong C_{\vee}^{S}(B)$ and $C_{\parallel}^{S}(B) \cong C_{\bullet}^{S}(B)$. There are no isomorphisms between these two pairs.

## 3.4 Some semiring maps

Let $S_{\wedge}(B)$ and $S_{\vee}(B)$ be, respectively, the semirings $(B, \wedge, \vee, 1, 0)$ and $(B, \vee, \wedge, 0, 1)$. We first observe that complementation is a semiring isomorphism for $S_{\wedge}(B)$ and $S_{\vee}(B)$. We define maps $\Delta_g: S_{\wedge}(B) \to C_{\wedge}^{S}(B)$ and $\iota_g: S_{\wedge}(B) \to C_{\parallel}^{S}(B)$ as follows: $\Delta_g(b) = (\neg b, b)$ and $\iota_g(b) = (1_B, b)$.
**Proposition 14.** $\Delta_g$ and $\iota_g$ are semiring homomorphisms.

Observe that $\Delta_g$ can be used to obtain a semiring map from $\mathbf{S}_\vee(B)$ to $\mathbf{C}_\vee^S(B)$ using the semiring isomorphisms $\neg : \mathbf{S}_\wedge(B) \xrightarrow{\sim} \mathbf{S}_\vee(B)$ and $(\cdot)^{-1} : \mathbf{C}_\wedge^S(B) \xrightarrow{\sim} \mathbf{C}_\vee^S(B)$ as follows:

$$ \begin{array}{ccc} \mathbf{S}_\vee(B) & \xrightarrow{\neg} & \mathbf{S}_\wedge(B) \\ \mathbf{S}_\vee(B) & \xrightarrow{\Delta_g} & \mathbf{C}_\wedge^S(B) \\ \mathbf{C}_\wedge^S(B) & \xrightarrow{(\cdot)^{-1}} & \mathbf{C}_\vee^S(B) \end{array} $$

This means that $\Delta_g$ is also a semiring homomorphism $\mathbf{S}_\vee(B) \xrightarrow{\Delta_g} \mathbf{C}_\vee^S(B)$. The following diagram commutes in the category of semirings:

$$ \begin{array}{ccc} \mathbf{S}_\wedge(B) & \xleftarrow{\neg} & \mathbf{S}_\vee(B) \\ \mathbf{S}_\wedge(B) & \xrightarrow{\sim} & \mathbf{S}_\vee(B) \\ \mathbf{C}_\wedge^S(B) & \xleftarrow{\sim} & \mathbf{C}_\vee^S(B) \end{array} $$

The commutativity of the diagram gives rise to the diagonal arrow $\Delta_a = (\cdot)^{-1} \circ \Delta_g = \Delta_g \circ \neg$. This map is a semiring homomorphism from $\mathbf{S}_\wedge(B)$ to $\mathbf{C}_\wedge^S(B)$ and from $\mathbf{S}_\vee(B)$ to $\mathbf{C}_\wedge^S(B)$. Explicitly, this map is

$$ \Delta_a b = (\Delta_g(b))^{-1} = (\neg b, b)^{-1} = (b, \neg b) \quad (b \in B). $$

If we use the map $\iota_g$, we can obtain $\iota'_a : \mathbf{S}_\vee(B) \to \mathbf{C}_\bullet^S(B)$ as follows:

$$ \begin{array}{ccc} \mathbf{S}_\vee(B) & \xrightarrow{\neg} & \mathbf{S}_\wedge(B) \\ \mathbf{S}_\vee(B) & \xrightarrow{\iota_g} & \mathbf{C}_\parallel^S(B) \\ \mathbf{C}_\parallel^S(B) & \xrightarrow{(\cdot)^{-1}} & \mathbf{C}_\vee^S(B) \end{array} $$

We obtain the diagram below.

$$ \begin{array}{ccc} \mathbf{S}_\wedge(B) & \xleftarrow{\neg} & \mathbf{S}_\vee(B) \\ \mathbf{S}_\wedge(B) & \xrightarrow{\sim} & \mathbf{S}_\vee(B) \\ \mathbf{C}_\wedge^S(B) & \xleftarrow{\sim} & \mathbf{C}_\vee^S(B) \end{array} $$

The commutativity of the diagram provides the semiring maps $\mathbf{S}_\wedge(B) \xrightarrow{\iota_a} \mathbf{C}_\bullet^S(B)$ and $\mathbf{S}_\vee(B) \xrightarrow{\iota'_g} \mathbf{C}_\parallel^S(B)$ given by $\iota_a = (\cdot)^{-1} \circ \iota_g$ and $\iota'_g = \iota_g \circ \neg$.

Now we consider maps to $\mathbf{S}_\wedge(B)$. The map $\pi_g : (a, g) \mapsto g$ is a semiring homomorphism from $\mathbf{C}_\wedge^S(B)$ to $\mathbf{S}_\wedge(B)$ and from $\mathbf{C}_\parallel^S(B)$ to $\mathbf{S}_\wedge(B)$. Similarly, the
map $\pi'_a : (a,g) \mapsto \neg a$ is a semiring homomorphism from $C_\wedge^S(B)$ to $S_\wedge(B)$. The following diagrams commute and define the maps not specified before.

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

# 4 Actions

One of the questions we sought to answer was: how can we compute contract abstractions? Abstractions are useful to carry out refinement verification in less costly computational environments. We will define abstractions through contract actions.

The semiring maps just described can be used to generate actions of the semirings $S_\wedge(B)$ and $S_\vee(B)$ over the contract semirings. Consider, for example the map $\Delta_g : S_\wedge(B) \to C_\wedge^S(B)$. For a contract $C = (a,g)$, we have $\Delta_g(b) \wedge C = (\neg b, b) \wedge (a,g) = (b \to a, b \wedge g)$.

Now consider the map $\iota_g : S_\wedge(B) \to C_\parallel^S(B)$; $\iota_g(b) \parallel C = (1_B, b) \parallel (a,g) = ((b \wedge g) \to a, b \wedge g) = (b \to a, b \wedge g)$. We observe that $S_\wedge(B)$ acts in the same way on the semirings $C_\wedge^S(B)$ and $C_\parallel^S(B)$. This leads us to

**Definition 10.** The right action of $B$ on $C(B)$ is $(a,g) \cdot b = (b \to a, b \wedge g)$.

Similarly, the semiring map $\Delta_a : S_\wedge(B) \to C_\vee^S(B)$ yields $\Delta_a(b) \vee C = (b, \neg b) \vee (a,g) = (b \wedge a, b \to g)$, and the semiring map $\iota_a : S_\wedge(B) \to C_\bullet^S(B)$ results in $\iota_a(b) \bullet C = (b, 1_B) \bullet (a,g) = (b \wedge a, b \to g)$. $S_\wedge(B)$ acts in the same way on the semirings $C_\vee^S(B)$ and $C_\bullet^S(B)$. We thus obtain

**Definition 11.** The left action of $B$ on $C(B)$ is given by $b \cdot (a,g) = (b \wedge a, b \to g)$.

The left and right actions have the practical meaning of adding assumptions or guarantees, respectively, to a contract. The following proposition shows several properties of these actions.

**Proposition 15.** The identities for the left and right actions shown in Table 4 hold.

The left action on contracts can be used to generate an abstraction for the guarantees of a contract. Given a contract $C$ and $b \in B$, we know from Table 4 that $C \le b \cdot C$. This tells us that we can obtain a more relaxed contract by adding assumptions. Subsequently, we may make use of this additional assumption to coarsen the guarantees of the contract. This operation is rich in algebraic properties, as shown in Table 4. For algorithmic manipulations of contracts, see Chapter 7 of [14].
<table><caption>Table 4: Identities for the left and right actions of a Boolean algebra $\bar{B}$ over its contract algebra $(b, b' \in B)$ and $C, C' \in C(B)$</caption><thead><tr><th>Order</th><th>C · b ≤ C</th></tr></thead><tbody><tr><td>b · C ≥ C<br>C ≤ C' ⇒ b · C ≤ b · C'</td><td>C ≤ C' ⇒ C · b ≤ C' · b</td></tr><tr><td colspan="2">Reciprocal<br>(b · C)<sup>-1</sup> = C<sup>-1</sup> · b</td></tr><tr><td colspan="2">Associativity<br>(b ∧ b') · C = b · (b' · C)</td></tr><tr><td colspan="2">Distributivity over the Boolean algebra<br>(b ∨ b') · C = (b · C) ∧ (b' · C)</td></tr><tr><td colspan="2">Actions and the contract operations<br>b · (C ∧ C') = b · C ∧ b · C'<br>b · (C ∨ C') = b · C ∨ C'<br>b · (C || C') = b · C || b · C'<br>b · (C · C') = b · C · C'</td></tr><tr><td colspan="2">Actions and the adjoint operations<br>b · (C/C') = C/(C' · b) = (b · C)/C'<br>b · (C ÷ C') = (b · C) ÷ (C' · b)<br>b · (C' → C) = C' → b · C = C' · b → C<br>b · (C' → C) = C' · b → b · C</td></tr></tbody></table>

# 5 Contract abstractions

It is often useful to vary the level of detail used to represent objects. More detail may be needed to carry out some analysis tasks, but too much detail may hinder computation. We will explore Question 2: how can we compute contract abstractions?

## 5.1 The Galois-connection abstraction

Suppose we have a monotone operator $\alpha: B_c \to B_a$, where $B_a$ and $B_c$ are Boolean algebras called abstract and concrete domains, respectively. Suppose that $\alpha$ is also a monoid map $\alpha: M_{\vee}(B_c) \to M_{\vee}(B_a)$, i.e., it commutes with disjunction and maps $1_{B_c}$ to $1_{B_a}$. We can define a map $\bar{\alpha}: C(B_c) \to C(B_a)$ as

$$ \bar{\alpha}: (a, g) \mapsto (\alpha(a), \alpha(g)). \qquad (3) $$

The map is well-defined since $\alpha(a) \vee \alpha(g) = \alpha(a \vee g) = \alpha(1_{B_c}) = 1_{B_a}$. Moreover, the monotonicity of $\bar{\alpha}$ follows from the monotonicity of $\alpha$. This abstraction is a slight generalization of that proposed in Chapter 5 of [4].

How can such a map $\alpha$ be obtained? Suppose that $\alpha$ is a monotone map that maps $1_{B_c}$ to $1_{B_a}$. If $\alpha$ is a left element of a Galois connection pair, then it commutes with disjunction (because left adjoints commute with colimits). Thus, such an $\alpha$ generates a valid contract abstraction (3).

## 5.2 Contract Galois connections from Boolean algebra maps

Let $f: B \to B'$ be a Boolean algebra map. $f$ induces a map $f^*: C(B) \to C(B')$ between their contract algebras given by $f^*(a, g) = (f(a), f(g))$. Observe that
$f(a) \lor f(g) = f(a \lor g) = f(1_B) = 1_{B'}$. As $f$ commutes with the Boolean algebra operations, $f^*$ commutes with the contract operations. Thus, $f^*$ is well-defined.

Let $\gamma : B_a \to B_c$ and $\alpha : B_c \to B_a$ be Boolean algebra maps. These maps generate contract maps $C(B_a) \xrightarrow{\gamma^*} C(B_c)$ and $C(B_c) \xrightarrow{\alpha^*} C(B_a)$, as described before.

We are interested in exploring the conditions needed for these maps to form a Galois connection. Specifically, for $C_a = (a_a, g_a) \in C(B_a)$ and $C_c = (a_c, g_c) \in C(B_c)$, we want $\alpha^*(C_c) \leq C_a$ if and only if $C_c \leq \gamma^*(C_a)$.

This means that $(\alpha a_c, \alpha g_c) \leq (a_a, g_a)$ if and only if $(a_c, g_c) \leq (\gamma a_a, \gamma g_a)$. If we set $a_c = 1_{B_c}$ and $a_a = 1_{B_a}$, we get $\alpha g_c \leq g_a$ if and only if $g_c \leq \gamma g_a$, and if we set $g_c = 1_{B_c}$ and $g_a = 1_{B_a}$, we obtain $a_a \leq \alpha a_c$ if and only if $\gamma a_a \leq a_c$.

This means that $\alpha$ and $\gamma$ must be simultaneously the left and right adjoints of each other. By setting $g_c = \gamma g_a$ and $a_c = \gamma a_a$ in the equations above, we obtain that $\alpha \circ \gamma$ is the identity map. Similarly, by setting $g_a = \alpha g_c$ and $a_a = \alpha a_c$, we get that $\gamma \circ \alpha$ is the identity map. This means that $B_a$ and $B_c$ are isomorphic. We conclude that contract Galois connections generated from Boolean algebra maps impose very rigid constraints on the Boolean algebras over which the contracts are defined.

# 6 Conclusions

Assume-guarantee contracts provide effective tools in system engineering design. In this paper, we described the algebra of contracts that can provide a framework for manipulating contracts in a structured way.

We explored in-depth this algebraic structure *per se*, while establishing a mathematically sound methodology for contract-based system design. The rich algebraic structure of assume-guarantee contracts provides sound support for a number of operations in system design: combining viewpoints, composing sub-specifications, and patching a design. At the same time, it raises a number of open methodological issues: does a designer have freedom in ordering the different design steps? Alternatively, does the theory impose or recommend an ordering? Abstractions are a well established way to provide semi-decision procedures at a lower computational cost. In this paper, we answered the following question: is there a systematic way to lift abstractions of properties to abstractions of contracts?

While writing assume-guarantee contracts is intuitive in applications, the computation of the algebraic operations is often not. Pacti<fnref n="6" /> was recently introduced [15] to support the design tasks that are backed by the algebra of contracts. Pacti is able to automatically compute several of the operations we discussed.

An important question remains open: is there a sound way to lift testing from properties—where this is well-developed—to assume-guarantee contracts? Our algebra of assume-guarantee contracts does not provide answers to this question as yet.

<footnote n="6">⁶ https://www.pacti.org</footnote>
References

1. Abadi, M., Lamport, L.: Composing specifications. ACM Transactions on Programming Languages and Systems 15(1), 73-132 (Jan 1993). https://doi.org/10.1145/151646.151649, http://doi.acm.org/10.1145/151646.151649

2. de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering. pp. 109-120. ESEC/FSE-9, Association for Computing Machinery, New York, NY, USA (2001). https://doi.org/10.1145/503209.503226, https://doi.org/10.1145/503209.503226

3. Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., Willem-Paul de Roever (eds.) Formal Methods for Components and Objects, 6th International Symposium (FMCO 2007), Amsterdam, The Netherlands, October 24-26, 2007, Revised Papers, Lecture Notes in Computer Science, vol. 5382, pp. 200-225. Springer Verlag, Berlin Heidelberg (2008). https://doi.org/10.1007/978-3-540-92188-2

4. Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinkemeier, P., Sangiovanni-Vincentelli, A.L., Damm, W., Henzinger, T.A., Larsen, K.G.: Contracts for system design. Foundations and Trends® in Electronic Design Automation 12(2-3), 124-400 (2018)

5. Damm, W.: Controlling speculative design processes using rich component models. In: Fifth International Conference on Application of Concurrency to System Design (ACSD'05). pp. 118-119 (June 2005). https://doi.org/10.1109/ACSD.2005.35

6. Davies, A., Brady, T., Hobday, M.: Organizing for solutions: Systems seller vs. systems integrator. Industrial marketing management 36(2), 183-193 (2007)

7. Emes, M., Smith, A., Cowper, D.: Confronting an identity crisis—how to “brand” systems engineering. Systems Engineering 8(2), 164-186 (2005). https://doi.org/https://doi.org/10.1002/sys.20028, https://onlinelibrary.wiley.com/doi/abs/10.1002/sys.20028

8. Floyd, R.W.: Assigning meanings to programs. Mathematical Aspects of Computer Science, ed. Schwartz, JT, Amer. Math. Soc (1967)

9. Golan, J.S.: Semirings and their Applications. Springer, Dordrecht, 1st ed edn. (1999). https://doi.org/10.1007/978-94-015-9333-5

10. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576-580 (Oct 1969). https://doi.org/10.1145/363235.363259, http://doi.acm.org/10.1145/363235.363259

11. Hobday, M., Davies, A., Prencipe, A.: Systems integration: a core capability of the modern corporation. Industrial and corporate change 14(6), 1109-1143 (2005)

12. Iannopollo, A., Nuzzo, P., Tripakis, S., Sangiovanni-Vincentelli, A.: Library-based scalable refinement checking for contract-based design. In: 2014 Design, Automation & Test in Europe Conference & Exhibition (DATE). pp. 1-6. IEEE (2014)

13. Incer, I., Sangiovanni-Vincentelli, A.L., Lin, C.W., Kang, E.: Quotient for assume-guarantee contracts. In: 16th ACM-IEEE International Conference on Formal Methods and Models for System Design. pp. 67-77. MEMOCODE'18 (October 2018). https://doi.org/10.1109/MEMCOD.2018.8556872

14. Incer, I.: The Algebra of Contracts. Ph.D. thesis, EECS Department, University of California, Berkeley (May 2022)
15. Incer, I., Badithela, A., Graebener, J., Mallozzi, P., Pandey, A., Yu, S.J., Benveniste, A., Caillaud, B., Murray, R.M., Sangiovanni-Vincentelli, A., et al.: Pacti: Scaling assume-guarantee reasoning for system analysis and design. arXiv preprint arXiv:2303.17751 (2023)

16. Incer, I., Mangeruca, L., Villa, T., Sangiovanni-Vincentelli, A.L.: The quotient in preorder theories. In: Raskin, J.F., Bresolin, D. (eds.) Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, Brussels, Belgium, September 21-22, 2020. Electronic Proceedings in Theoretical Computer Science, vol. 326, pp. 216-233. Open Publishing Association, Brussels, Belgium (2020). https://doi.org/10.4204/EPTCS.326.14

17. Jackson, S.: Memo to industry: The crisis in systems engineering. INSIGHT 13(1), 43-43 (2010). https://doi.org/https://doi.org/10.1002/inst.201013143; https://onlinelibrary.wiley.com/doi/abs/10.1002/inst.201013143

18. Lamport, L.: A simple approach to specifying concurrent systems. Commun. ACM 32(1), 32-45 (Jan 1989). https://doi.org/10.1145/63238.63240; http://doi.acm.org/10.1145/63238.63240

19. Leveson, N.: A new accident model for engineering safer systems. Safety Science 42(4), 237-270 (2004). https://doi.org/https://doi.org/10.1016/S0925-7535(03)00047-X; https://www.sciencedirect.com/science/article/pii/S092575350300047X

20. Madni, A.M., Sievers, M.: Systems integration: Key perspectives, experiences, and challenges. Systems Engineering 17(1), 37-51 (2014). https://doi.org/https://doi.org/10.1002/sys.21249; https://onlinelibrary.wiley.com/doi/abs/10.1002/sys.21249

21. Mallozzi, P., Nuzzo, P., Pelliccione, P.: Incremental refinement of goal models with contracts. In: Hojjat, H., Massink, M. (eds.) Fundamentals of Software Engineering. pp. 35-50. Springer International Publishing, Cham (2021)

22. Meyer, B.: Applying "design by contract". IEEE Computer 25(10), 40-51 (October 1992). https://doi.org/10.1109/2.161279

23. National Defense Industrial Association and others: Top systems engineering issues in US defense industry. Systems Engineering Division Task Group Report (2016)

24. Negulescu, R.: Process spaces. Tech. Rep. CS-95-48, University of Waterloo (1995)

25. Nuzzo, P., Sangiovanni-Vincentelli, A.L., Bresolin, D., Geretti, L., Villa, T.: A platform-based design methodology with contracts and related tools for the design of cyber-physical systems. Proceedings of the IEEE 103(11), 2104-2132 (2015). https://doi.org/10.1109/JPROC.2015.2453253

26. Passerone, R., Incer, I., Sangiovanni-Vincentelli, A.L.: Coherent extension, composition, and merging operators in contract models for system design. ACM Trans. Embed. Comput. Syst. 18(5s) (Oct 2019). https://doi.org/10.1145/3358216

27. Sage, A.P., Lynch, C.L.: Systems integration and architecting: An overview of principles, practices, and perspectives. Systems Engineering: The Journal of The International Council on Systems Engineering 1(3), 176-227 (1998)

28. Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming dr. frankenstein: Contract-based design for cyber-physical systems. European journal of control 18(3), 217-238 (2012)

29. Sangiovanni-Vincentelli, A.L., Damm, W., Passerone, R.: Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems. European Journal of Control 18(3), 217-238 (2012). https://doi.org/http://dx.doi.org/10.3166/ejc.18.217-238; http://www.sciencedirect.com/science/article/pii/S0947358012709433
## A Proofs

*Proof of Proposition 6.* Let $C_i$ be the contract stated in the proposition. Observe that $C_i \wedge C' = C \wedge C'$. Thus, by the monotonicity of conjunction, $C'' \leq C_i$ implies that $C'' \wedge C' \leq C$.

Now write $C''$ as $C'' = (A'', G'')$ and assume that $C'' \wedge C' \leq C$. Then

$$G'' \cap G' \leq G \text{ and} \\ A'' \cup A' \geq A.$$

From this we conclude that

$$G'' \leq G \cup \neg G' \text{ and} \qquad (4)$$

$$A'' \geq A \cap \neg A'. \qquad (5)$$

From (4) and the fact that $A'' \geq \neg G''$ (which follows from the definition of AG contracts), we obtain $A'' \geq G' \cap \neg G$. This result and (5) yield

$$A'' \geq (A \cap \neg A') \cup (G' \cap \neg G).$$

This expression and (4) mean that $C'' \leq C_i$, completing the proof. □

*Proof of Proposition 8.* We already know that 1 and 0 are, respectively, the identity elements of conjunction and disjunction. $e$ is the identity for composition and merging. The idempotence of these operations follows immediately from their definitions. It remains to show that these operations are associative.

Let $C = (a, g)$, $C' = (a', g')$, and $C'' = (a'', g'')$ be contracts.

– Conjunction.

$$\begin{align*} C \wedge (C' \wedge C'') &= (a, g) \wedge (a' \vee a'', g' \wedge g'') \\ &= (a \vee (a' \vee a''), g \wedge (g' \wedge g'')) \\ &= ((a \vee a') \vee a'', (g \wedge g') \wedge g'') \\ &= (a \vee a', g \wedge g') \wedge C'' = (C \wedge C') \wedge C'' \end{align*}$$

– Disjunction.

$$\begin{align*} C \vee (C' \vee C'') &= (C^{-1} \wedge ((C')^{-1} \wedge (C'')^{-1}))^{-1} \\ &= ((C^{-1} \wedge (C')^{-1}) \wedge (C'')^{-1})^{-1} = (C \vee C') \vee C'' \end{align*}$$

– Composition.

$$\begin{align*} C \parallel (C' \parallel C'') \\ &= (a, g) \parallel (\neg g' \vee \neg g'' \vee (a' \wedge a''), g' \wedge g'') \\ &= (\neg g \vee \neg g' \vee \neg g'' \vee (a \wedge a' \wedge a''), g \wedge (g' \wedge g'')) \\ &= (\neg g \vee \neg g' \vee \neg g'' \vee ((a \wedge a') \wedge a''), (g \wedge g') \wedge g'') \\ &= (\neg g \vee \neg g' \vee (a \wedge a'), g \wedge g') \parallel C'' = (C \parallel C') \parallel C'' \end{align*}$$
Because $\pi$ is epic, $f^{\#}$ generates a unique monoid map $f^{\flat}$

$$ \begin{tikzcd} \mathbf{M}_{\wedge}(B) \times \mathbf{M}_{\wedge}(B) \arrow[r, "f^{\flat}"] \arrow[d, "\pi"] & \mathbf{M}_{\wedge}(B') \times \mathbf{M}_{\wedge}(B') \arrow[d, "\iota"] \\ \mathbf{C}_{\parallel}^{M}(B) \arrow[r, "f^{\#}", "\text{------}\xrightarrow{f}"] \arrow[d, "f"] & \mathbf{C}_{\parallel}^{M}(B') \arrow[r, "\iota"] \arrow[d, "f^{\#}", "\text{------}\xrightarrow{f}"] \end{tikzcd} $$

Thus, we have the diagram

$$ \begin{tikzcd} \mathbf{M}_{\wedge}(B) \times \mathbf{M}_{\wedge}(B) \arrow[r, "f^{\flat}"] \arrow[d, "\pi"] & \mathbf{M}_{\wedge}(B') \times \mathbf{M}_{\wedge}(B') \arrow[d, "\iota", "\text{------}\xrightarrow{\pi}"] \\ \mathbf{C}_{\parallel}^{M}(B) \arrow[r, "f^{\#}", "\text{------}\xrightarrow{f}"] \arrow[d, "f"] & \mathbf{C}_{\parallel}^{M}(B') \arrow[r, "\iota", "\text{------}\xrightarrow{\iota}"] \end{tikzcd} \quad (6) $$

$f^{\flat}$ can be factored as the product of two maps

$$ \mathbf{M}_{\wedge}(B) \times \mathbf{M}_{\wedge}(B) \to \mathbf{M}_{\wedge}(B'). $$

We also observe that $f^{\flat}(a, g) = f^{\flat}((a, 1) \wedge (1, g)) = f^{\flat}(a, 1) \wedge f^{\flat}(1, g)$. This means there are monoid maps $l_a, l_g, r_a, r_g: \mathbf{M}_{\wedge}(B) \to \mathbf{M}_{\wedge}(B')$ such that

$$ f^{\flat}(a, g) = (l_a(a)l_g(g), r_a(a)r_g(g)). $$

To obtain further restrictions on these maps, we use (6): $f^{\flat}(a, g) = \iota \circ f \circ \pi(a, g) = \iota \circ \pi \circ f^{\flat} \circ \iota \circ \pi(a, g) = (l_a(ag)l_g(g)r_a(ag)r_g(g), r_a(ag)r_g(g)). \square$

*Proof of Proposition 10.* Let $C = (a, g)$, $C' = (a', g')$, and $C'' = (a'', g'')$ be contracts.

– Conjunction.

$$ \begin{align*} C \wedge (C' \vee C'') &= (a, g) \wedge (a' \wedge a'', g' \vee g'') \\ &= ((a \vee a') \wedge (a \vee a''), (g \wedge g') \vee (g \wedge g'')) \\ &= (C \wedge C') \vee (C \wedge C'') \end{align*} $$

$$ \begin{align*} C \wedge (C' \parallel C'') &= (a, g) \wedge ((g' \wedge g'') \to (a' \wedge a''), g' \wedge g'') \\ &= (a \vee (a' \wedge a'') \vee \neg g' \vee \neg g'', g \wedge g' \wedge g'') \\ &= (a \vee \neg g \vee (a' \wedge a'') \vee \neg g' \vee \neg g'', g \wedge g' \wedge g'') \\ &= ((g \wedge g' \wedge g'') \to ((a \vee a') \wedge (a \vee a'')), g \wedge g' \wedge g'') \\ &= (a \vee a', g \wedge g') \parallel (a \vee a'', g \wedge g'') \\ &= (C \wedge C') \parallel (C \wedge C'') \end{align*} $$

$$ \begin{align*} e \wedge (1 \bullet 0) &= e \wedge 1 = e \neq 0 \\ &= e \bullet 0 = (e \wedge 1) \bullet (e \wedge 0) \end{align*} $$
– Disjunction.

$$
\begin{align*}
C \lor (C' \land C'') &= (C^{-1} \land ((C')^{-1} \lor (C'')^{-1}))^{-1} \\
&= ((C^{-1} \land (C')^{-1}) \lor (C^{-1} \land (C'')^{-1}))^{-1} \\
&= (C \lor C') \land (C \lor C'')
\end{align*}
$$

$$
\begin{align*}
C \lor (C' \bullet C'') &= (C^{-1} \land ((C')^{-1} \| (C'')^{-1}))^{-1} \\
&= ((C^{-1} \land (C')^{-1}) \| (C^{-1} \land (C'')^{-1}))^{-1} \\
&= (C \lor C') \bullet (C \lor C'')
\end{align*}
$$

$$
\begin{align*}
e \lor (1 \parallel 0) &= e \lor 0 = e \neq 1 \\
&= 1 \parallel e = (e \lor 1) \parallel (e \lor 0)
\end{align*}
$$

– Composition.

$$
\begin{align*}
C \parallel (C' \land C'') &= (a, g) \parallel (a' \lor a'', g' \land g'') \\
&= \left( \begin{array}{@{}l@{}}
  \neg(g \land g') \lor \neg(g \land g'') \lor (a \land a') \lor (a \land a''), \\
  (g \land g') \land (g \land g'')
\end{array} \right) \\
&= ((g \land g') \rightarrow (a \land a'), (g \land g')) \land \\
&\qquad ((g \land g'') \rightarrow (a \land a''), (g \land g'')) \\
&= (C \parallel C') \land (C \parallel C'')
\end{align*}
$$

$$
\begin{align*}
C \parallel (C' \lor C'') &= (a, g) \parallel (a' \land a'', g' \lor g'') \\
&= \left( \begin{array}{@{}l@{}}
  \neg(g \land g') \land \neg(g \land g'') \lor ((a \land a') \land (a \land a'')), \\
  (g \land g') \lor (g \land g'')
\end{array} \right) \\
&= \left( \begin{array}{@{}l@{}}
  \neg(g \land g') \lor (a \land a') \land \neg(g \land g'') \lor (a \land a''), \\
  (g \land g') \lor (g \land g'')
\end{array} \right) \\
&= ((g \land g') \rightarrow (a \land a'), (g \land g')) \\
&\quad \lor ((g \land g'') \rightarrow (a \land a''), (g \land g'')) \\
&= (C \parallel C') \lor (C \parallel C'')
\end{align*}
$$

$$
\begin{align*}
1 \parallel (0 \bullet e) &= 1 \parallel 0 = 0 \neq 1 = 0 \bullet 1 \\
&= (1 \parallel 0) \bullet (1 \parallel e)
\end{align*}
$$

The distributivity of composition over conjunction was shown in [21].

– Merging.

$$
\begin{align*}
C \bullet (C' \land C'') &= (C^{-1} \parallel ((C')^{-1} \lor (C'')^{-1}))^{-1} \\
&= ((C^{-1} \parallel (C')^{-1}) \lor (C^{-1} \parallel (C'')^{-1}))^{-1} \\
&= (C \bullet C') \land (C \bullet C'')
\end{align*}
$$

$$
\begin{align*}
C \bullet (C' \lor C'') &= (C^{-1} \parallel ((C')^{-1} \land (C'')^{-1}))^{-1} \\
&= ((C^{-1} \parallel (C')^{-1}) \land (C^{-1} \parallel (C'')^{-1}))^{-1}
\end{align*}
$$
$$ 
\begin{aligned}
&= (\mathcal{C} \bullet \mathcal{C}') \vee (\mathcal{C} \bullet \mathcal{C}'') \\
0 \bullet (1 \parallel e) &= 0 \bullet 1 = 1 \neq 0 = 1 \parallel 0 \\
&= (0 \bullet 1) \parallel (0 \bullet e)
\end{aligned}
$$

□

*Proof of Proposition 11.* Due to the distributivity of ⋆ over conjunction and disjunction (Proposition 10), we have $(C_1 \wedge C_2) \star (C_3 \wedge C_4) = (C_1 \star C_3) \wedge (C_1 \star C_4) \wedge (C_2 \star C_3) \wedge (C_2 \star C_4) \le (C_1 \star C_3) \wedge (C_2 \star C_4)$ and $(C_1 \vee C_2) \star (C_3 \vee C_4) = (C_1 \star C_3) \vee (C_1 \star C_4) \vee (C_2 \star C_3) \vee (C_2 \star C_4) \ge (C_1 \star C_3) \vee (C_2 \star C_4)$. □

*Proof of Proposition 12.* Tables 2 and 3 tell, respectively, how operations behave with respect to the distinguished elements and how operations distribute.

Suppose conjunction is the multiplication operation. Since $\mathcal{C} \wedge e \neq e$, neither merging nor composition can be the addition operations. On the other hand, $\mathcal{C} \wedge 0 = 0$, and conjunction distributes over disjunction. Thus, $(\mathcal{C}(B), \wedge, \vee, 1, 0)$ is a semiring.

Now we assume disjunction is the multiplication operation. Since $\mathcal{C} \vee e \neq e$, neither merging nor composition can be the addition operations. However, $\mathcal{C} \vee 1 = 1$, and disjunction distributes over conjunction. Thus, $(\mathcal{C}(B), \vee, \wedge, 0, 1)$ is a semiring.

Suppose composition is the multiplication operation. Since composition does not distribute over merging, merging cannot be addition. Since $\mathcal{C} \parallel 1 \neq 1$, conjunction cannot be addition. However, $\mathcal{C} \parallel 0 = 0$ and composition distributes over disjunction. Thus, $(\mathcal{C}(B), \parallel, \vee, e, 0)$ is a semiring.

Now suppose that merging is the multiplication. Since merging does not distribute over composition, composition cannot be addition. Also, since $\mathcal{C} \bullet 0 \neq 0$, conjunction cannot be addition. However, $\mathcal{C} \bullet 1 = 1$ and merging distributes over conjunction. Thus, $(\mathcal{C}(B), \bullet, \wedge, e, 1)$ is a semiring. □

*Proof of Proposition 13.* The two semiring isomorphisms are given by the reciprocal map. Suppose there is a semiring map $\beta: \mathcal{C}_{\parallel}^{S}(B) \to \mathcal{C}_{\wedge}^{S}(B)$. Then

$$ \beta(a, 1_B) = \beta((a, 1_B) \vee e) = \beta(a, g) \vee 1 = 1, $$

which means that $\beta$ is not invertible.

□

*Proof of Proposition 14.* Let $b, b' \in B$.

$$ - \Delta_g(0_B) = (1_B, 0_B) = 0 \text{ and } \Delta_g(1_B) = (0_B, 1_B) = 1 $$

$$ - \Delta_g(b \wedge b') = (\neg(b \wedge b'), b \wedge b') = (\neg b \vee \neg b', b \wedge b') = \Delta_g(b) \wedge \Delta_g(b') $$

$$ - \Delta_g(b \vee b') = (\neg(b \vee b'), b \vee b') = (\neg b \wedge \neg b', b \vee b') = \Delta_g(b) \vee \Delta_g(b') $$

This shows that $\Delta_g$ is a semiring homomorphism. Now we study $\iota_g$:

$$ - \iota_g(0_B) = (1_B, 0_B) = 0 \text{ and } \iota_g(1_B) = (1_B, 1_B) = e $$

$$ - \iota_g(b \wedge b') = (1_B, b \wedge b') = (1_B, b) \parallel (1_B, b') = \iota_g(b) \parallel \iota_g(b') $$

$$ - \iota_g(b \vee b') = (1_B, b \vee b') = (1_B, b) \vee (1_B, b') = \iota_g(b) \vee \iota_g(b') $$

We conclude that $\iota_g$ is a semiring homomorphism as well.

□
*Proof of Proposition 15.* Let $b, b' \in B$, $C = (a, g)$, and $C' = (a', g')$. We have the following properties:

- Order.

$$ 
\begin{aligned}
b \cdot C &= b \cdot (a, g) = (b \wedge a, b \rightarrow g) \geq (a, g) = C \\
C \cdot b &= (a, g) \cdot b = (b \rightarrow a, b \wedge g) \leq (a, g) = C
\end{aligned}
$$

Now suppose $C = (a, g) \leq C' = (a', g')$. We have $a' \leq a$ and $g \leq g'$. Since the operations $b \wedge (\cdot)$ and $b \rightarrow (\cdot)$ are monotonic, we have $b \cdot C \leq b \cdot C'$ and $C \cdot b \leq C' \cdot b$.

- Reciprocal.

$$ 
\begin{aligned}
(b \cdot C)^{-1} &= (b \wedge a, b \rightarrow g)^{-1} = (b \rightarrow g, b \wedge a) \\
&= (g, a) \cdot b = C^{-1} \cdot b
\end{aligned}
$$

- Associativity.

$$ 
\begin{aligned}
(b \wedge b') \cdot C &= ((b \wedge b') \wedge a, (b \wedge b') \rightarrow g) \\
&= (b \wedge (b' \wedge a), b \rightarrow (b' \rightarrow g)) \\
&= b \cdot (b' \cdot (a, g)) = b \cdot (b' \cdot C) \\
C \cdot (b \wedge b') &= ((b \wedge b') \cdot C^{-1})^{-1} = ((b' \wedge b) \cdot C^{-1})^{-1} \\
&= (b' \cdot (b \cdot C^{-1}))^{-1} = (b \cdot C^{-1})^{-1} \cdot b' = (C \cdot b) \cdot b'
\end{aligned}
$$

- Distributivity over the Boolean algebra $B$.

$$ 
\begin{aligned}
(b \vee b') \cdot C &= ((b \vee b') \wedge a, (b \vee b') \rightarrow g) \\
&= ((b \wedge a) \vee (b' \wedge a), (b \rightarrow g) \wedge (b' \rightarrow g)) \\
&= (b \cdot C) \wedge (b' \cdot C) \\
C \cdot (b \vee b') &= ((b \vee b') \cdot C^{-1})^{-1} \\
&= (b \cdot C^{-1} \wedge b' \cdot C^{-1})^{-1} \\
&= C \cdot b \vee C \cdot b'
\end{aligned}
$$

- Distributivity over the contract operations.

• Conjunction.

$$ 
\begin{aligned}
b \cdot (C \wedge C') &= (b \wedge (a \vee a'), b \rightarrow (g \wedge g')) \\
&= ((b \wedge a) \vee (b \wedge a'), (b \rightarrow g) \wedge (b \rightarrow g')) \\
&= b \cdot C \wedge b \cdot C' \\
(C \wedge C') \cdot b &= (b \rightarrow (a \vee a'), b \wedge (g \wedge g')) \\
&= ((b \rightarrow a) \vee a', (b \wedge g) \wedge g') \\
&= (C \cdot b) \wedge C'
\end{aligned}
$$
• Disjunction.

$$
\begin{align*}
b \cdot (C \lor C') &= ((C^{-1} \land (C')^{-1}) \cdot b)^{-1} \\
&= (C^{-1} \cdot b \land (C')^{-1})^{-1} \\
&= b \cdot C \lor C'
\end{align*}
$$

$$
\begin{align*}
(C \lor C') \cdot b &= (b \cdot (C^{-1} \land (C')^{-1}))^{-1} \\
&= (b \cdot C^{-1} \land b \cdot (C')^{-1})^{-1} \\
&= C \cdot b \lor C' \cdot b
\end{align*}
$$

• Composition.

$$
\begin{align*}
b \cdot (C \parallel C')
  &= (b \land ((g \land g') \rightarrow (a \land a')) , b \rightarrow (g \land g')) \\
  &= \left( \begin{array}{@{}l@{}}
    (b \rightarrow (g \land g')) \rightarrow (b \land a \land a') , \\
    b \rightarrow (g \land g')
  \end{array} \right) \\
  &= \left( \begin{array}{@{}l@{}}
    ((b \rightarrow g) \land (b \rightarrow g')) \rightarrow ((b \land a) \land (b \land a')) , \\
    (b \rightarrow g) \land (b \rightarrow g')
  \end{array} \right) \\
  &= b \cdot C \parallel b \cdot C'
\end{align*}
$$

$$
\begin{align*}
(C \parallel C') \cdot b
  &= (b \rightarrow ((g \land g') \rightarrow (a \land a')) , b \land g \land g') \\
  &= ((b \land g \land g') \rightarrow (a \land a') , b \land g \land g') \\
  &= ((b \land g \land g') \rightarrow ((b \rightarrow a) \land a') , b \land g \land g') \\
  &= (C \cdot b) \parallel C'
\end{align*}
$$

• Merging.

$$
b \cdot (C \bullet C') = ((C^{-1} \parallel (C')^{-1}) \cdot b)^{-1} \\
= (C^{-1} \cdot b \parallel (C')^{-1})^{-1} = b \cdot C \bullet C'
$$

$$
\begin{align*}
(C \bullet C') \cdot b &= (b \cdot (C^{-1} \parallel (C')^{-1}))^{-1} \\
&= (b \cdot C^{-1} \parallel b \cdot (C')^{-1})^{-1} = C \cdot b \bullet C' \cdot b
\end{align*}
$$

– Distributivity over the adjoint operations.

• Quotient.

$$
\begin{align*}
b \cdot (C/C') &= b \cdot (C \bullet (C')^{-1}) = b \cdot C \bullet (C')^{-1} \\
&= (b \cdot C)/(C')
\end{align*}
$$

$$
\begin{align*}
b \cdot (C/C') &= b \cdot (C \cdot (C')^{-1}) = C \cdot b \cdot (C')^{-1} \\
&= C \cdot (C' \cdot b)^{-1} = C/(C' \cdot b)
\end{align*}
$$

$$
\begin{align*}
(C/C') \cdot b &= (C \cdot (C')^{-1}) \cdot b = C \cdot b \cdot (C')^{-1} \cdot b \\
&= C \cdot b \cdot (b \cdot C')^{-1} = (C \cdot b)/(b \cdot C')
\end{align*}
$$
• Separation.

$$ 
\begin{aligned}
b \cdot (C \div C') &= b \cdot (C \parallel (C')^{-1}) = b \cdot C \parallel b \cdot (C')^{-1} \\
&= b \cdot C \parallel (C' \cdot b)^{-1} = (b \cdot C) \div (C' \cdot b)
\end{aligned}
$$

$$ 
\begin{aligned}
(C \div C') \cdot b &= (C \parallel (C')^{-1}) \cdot b = C \cdot b \parallel (C')^{-1} \\
&= (C \cdot b) \div C'
\end{aligned}
$$

$$ 
\begin{aligned}
(C \div C') \cdot b &= (C \parallel (C')^{-1}) \cdot b \\
&= C \parallel (C')^{-1} \cdot b = C \div (b \cdot C')
\end{aligned}
$$

• Implication.

$$ 
\begin{aligned}
b \cdot (C' \to C) &= b \cdot ((a \land \neg a') \lor (g' \land \neg g), g \lor \neg g') \\
&= (b \land (a \land \neg a') \lor (b \land g' \land \neg g), (b \to g) \lor \neg g') \\
&= \left( \begin{array}{l} ((b \land a) \land \neg a') \lor (g' \land \neg (b \to g)), \\ (b \to g) \lor \neg g' \end{array} \right) \\
&= C' \to b \cdot C
\end{aligned}
$$

$$ 
\begin{aligned}
b \cdot (C' \to C) &= b \cdot ((a \land \neg a') \lor (g' \land \neg g), g \lor \neg g') \\
&= \left( \begin{array}{l} (a \land \neg (b \to a')) \lor (b \land g' \land \neg g), \\ (b \land g') \to g \end{array} \right) \\
&= C' \cdot b \to C
\end{aligned}
$$

$$ 
\begin{aligned}
(C' \to C) \cdot b &= ((a \land \neg a') \lor (g' \land \neg g), g \lor \neg g') \cdot b \\
&= \left( \begin{array}{l} (b \to (a \land \neg a')) \lor (b \to (g' \land \neg g)), \\ (b \land g) \lor \neg (b \to g') \end{array} \right) \\
&= \left( \begin{array}{l} (b \to a) \land \neg (b \land a') \lor (b \to g') \land \neg (b \land g), \\ (b \land g) \lor \neg (b \to g') \end{array} \right) \\
&= b \cdot C' \to C \cdot b
\end{aligned}
$$

• Coimplication.

$$ 
\begin{aligned}
b \cdot (C' \to C) &= (((C')^{-1} \to C^{-1}) \cdot b)^{-1} \\
&= (b \cdot (C')^{-1} \to C^{-1} \cdot b)^{-1} = C' \cdot b \to b \cdot C
\end{aligned}
$$

$$ 
\begin{aligned}
(C' \to C) \cdot b &= (b \cdot (((C')^{-1} \to C^{-1}))^{-1} \\
&= ((C')^{-1} \to b \cdot C^{-1})^{-1} = C' \to C \cdot b \\
&= ((C')^{-1} \cdot b \to C^{-1})^{-1} = b \cdot C' \to C
\end{aligned}
$$

□