Structural Contracts -- Contracts for Type Construction & Dependent Types to Ensure Consistency of Extra-Functional Reasoning

TL;DR

This paper introduces Structural Contracts, a method using type constraints and dependent types to ensure consistent and correct decomposition of contracts for extra-functional properties in software design.

Contribution

It proposes a novel approach combining type constraints and dependent types to improve contract-based design for extra-functional properties.

Findings

Defines the composition problem for contracts

Introduces the Structural Contracts approach

Ensures consistency in contract decomposition

Abstract

Targeting to use contract-based design for the specification and refinement of extra-functional properties, this research abstract suggests to use type constraints and dependent types to ensure correct and consistent top-down decomposition of contracts with respect to a specifiable type constructor. For this, we summarize the composition problem and give a short draft of our approach, called Structural Contracts.

Figures

Full text

\Footnotetext

This research is funded by the German Research Foundation (DFG) in the Research Training Group SCARE – System Correctness under Adverse Conditions (DFG-GRK 1765).

0.0.1 Motivation.

Design hierarchy and correct hierarchical reasoning are of great importance to manage the complexity of today’s system designs. By refining the system requirements – into a subsystem architecture and requirements of its parts – the complexity can be split up and the probability of design faults can be reduced. For this purpose, Contract Based Design (CBD) [1] is a formalism, which enables to specify and to formally verify such refinements.

In our approach we wish to reason about extra-functional properties (EFPs), by which we mean the formal specification and verification of properties and detection of faults which depend on multiple physical domains (quantities), as e. g. power consumption. To ensure safety, today’s distributed and reuse-oriented development processes must be able to reliably detect and prevent such faults when integrating electronic sensors and controllers within a safety-critical system.

Our goal is to use CBD for reasoning about these EFPs. For this, a specification and verification of domain-specific composition functions becomes necessary. We believe, this is not sufficiently considered in CBD, yet. Accordingly, this abstract gives an outline of this problem as well as of our approach of structural contracts (SCs), oriented on dependent types from constructive type theory. [6]

Outline of the Preliminaries.

The overall goal and concept of the CBD approach [1] is to specify and refine the requirements of a system $\hat{M}$ based on a contract $\hat{C}$ into $n\in\mathbb{N}$ contract-based specifications $\check{C}_{k\in K_{n}}$ of a set of $k\in K_{n}$-indexed subsystems $\check{M}^{*}\Coloneqq\{\check{M}_{1},\check{M}_{2},\ldots,\check{M}_{n}\}$ (where $K_{n}\Coloneqq\{1,\ldots,n\}\subseteq\mathbb{N}$), denoting its components. Fig. 1 gives a draft of this concept, sketching the refinement of a system $\hat{M}$ with the contract based specification $\hat{C}$ and its refinement into subsystems $\check{M}_{k}\in\check{M}^{*}$ with contracts $\check{C}_{k}$. Composing the components’ specifications $\check{C}_{k}$ to the composed specification $\check{C}\Coloneqq\otimes^{\mathbb{C}}_{k}\check{C}_{k}$ of the composed system $\check{M}\Coloneqq\otimes^{\mathbb{M}}_{k}\check{M}_{k}$ (with $\otimes^{\mathbb{M}}_{k}$ denoting k-ary composition over the set $\mathbb{M}$ of components and $\otimes^{\mathbb{C}}_{k}$ denoting k-ary composition over the set $\mathbb{C}$ of contracts) the refinement relation $\check{C}\preceq^{\mathbb{C}}\hat{C}$ can be verified.

For this, a contract $C\Coloneqq(A,G)$ formally describes a requirement by separated assertions $A$ and $G$, denoting the assumptions $A$ a component expects from its embedding environment, plus the corresponding guarantees $G$, which are provided for the case that the assumptions hold (formally ${A\rightarrow G}$). Semantically, the contracts are interpreted into $\mathbb{M}$ such that $[\![\cdot]\!]^{\mathbb{C}}:\mathbb{C}\rightarrow\mathfrak{P}^{2}_{\mathbb{M}}$ with $[\![C]\!]\Coloneqq(\mathcal{E},\mathcal{M})$ where $\mathfrak{P}_{\mathbb{M}}$ denotes the powerset over $\mathbb{M}$ and $\mathcal{E},\mathcal{M}\subseteq\mathbb{M}$ denotes the contracts’ sets of compatible environments and consistent implementations, respectively. Furthermore, two satisfaction relations $\models^{\mathcal{E}},\models^{\mathcal{M}}\subseteq\mathbb{M}\times\mathbb{C}$ are defined such that ${(E\models^{\mathcal{E}}C)}\Leftrightarrow{(E\in\mathcal{E})}$ and ${(M\models^{\mathcal{M}}C)}\Leftrightarrow{(M\in\mathcal{M})}$. Based on that, to compositionally reason about contracts, the composition operation $\otimes^{\mathbb{C}}_{k\in K_{n}}:\mathbb{C}^{n}\rightarrow\mathbb{C}$ is defined for $n$ contracts $\check{C}_{k}$, such that $\otimes^{\mathbb{C}}_{k\in K_{n}}\check{C}_{k}\Coloneqq$

\textit{min}\left\{\!{\check{C}\!\in\!\mathbb{C}}\!:\left[\begin{array}[]{l}\forall\hat{E}\!\in\!\mathbb{M},\\ \forall{\check{M}_{k\in K_{n}}}\!\in\!\mathbb{M}\end{array}\right]:\left[\begin{array}[]{l}{(\hat{E}\models^{\mathcal{E}}\!\check{C})}{\land}\\ \bigwedge_{k\in K_{n}}\!{(\check{M}_{k}\models^{\mathcal{M}}\!\check{C}_{k})}\end{array}\right]\rightarrow\left[\begin{array}[]{l}{\bigwedge_{k\in K_{n}}\!((\hat{E}\otimes^{\mathbb{M}}\!(\otimes^{\mathbb{M}}_{(j\neq k)\in K_{n}}\check{M}_{j}))\models^{\mathcal{E}}\!\check{C}_{k})}\\ \land\,{(\otimes^{\mathbb{M}}_{k\in K_{n}}\!\check{M}_{k}\models^{\mathcal{M}}\!\check{C})}\end{array}\right]\right\}

Please note that the composition operation $\otimes^{\mathbb{M}}:\mathbb{M}^{2}\rightarrow\mathbb{M}$ (resp. $\otimes^{\mathbb{M}}_{k}:\mathbb{M}^{n}\rightarrow\mathbb{M}$) over components is described as a part of our problem statement (cf. Sec. 0.0.2).

With that, the three main verification rules of CBD are: checking compatibility ($\mathcal{E}\neq\varnothing$ ?) and consistency ($\mathcal{M}\neq\varnothing$ ?) of all contracts, and checking refinement ($(\check{C}\preceq^{\mathbb{C}}\hat{C})\Leftrightarrow((\hat{\mathcal{E}}\subseteq\check{\mathcal{E}})\land(\hat{\mathcal{M}}\supseteq\check{\mathcal{M}}))$) between the system specification $\hat{C}$ and the composed specification $\check{C}=\otimes^{\mathbb{C}}_{k}\check{C}_{k}$ of the composed subsystems $\check{M}_{k}\in\check{M}^{*}$.

0.0.2 Problem Description.

We wish to introduce our problem based on an example from electronics (cf. Fig. 2) where we compose two resistors $\check{M}_{1}$, $\check{M}_{2}$ in series, resulting in a composed resistor $\check{M}$. For this composition, we examine how the equivalent electrical resistance $\check{M}.r$ results from $\check{M}_{1}.r$ and $\check{M}_{2}.r$. Considering $\mathbb{M}$ to reflect components from simple electrodynamic circuit theory, those follow Ohm’s Law ($R=u/i$) for resistors, constraining the voltage $u$ across and the current $i$ through any resistor. Furthermore, each node $e\!\in\!\{e_{0},e_{1},e_{\bot}\}$ satisfies Kirchhoffs Current Law ($\sum_{k\in K_{e}}i_{k}\!=\!0$), where $K_{e}\!\subseteq\!\{0,1,2\}$ defines the subsets $M_{e}\Coloneqq\{\check{M}_{k}:k\!\in\!K_{e}\}$ of the components that are connected by $e$. Finally, due to Kirchhoffs Voltage Law and the Law of Superposition, the branches $b\in\{(e_{j},e_{k}):j,k\in\{0,1,\bot\}\}$ satisfy ${u_{e_{j}}\!-\!u_{e_{k}}}=u_{m}$ for all branch components $M_{m}\!\in\!{K_{e_{j}}\!\cap\!K_{e_{k}}}$. Abbreviating (sub-)component properties $\check{M}.p$ with $\check{p}$ and $\check{M}_{k}.p$ with $\check{p}_{k}$ (i. e. ${\forall p\in\{r,u,i\}}:{\forall k\!\in\!\{0,1,2\}}:{\check{M}_{k}.p\equiv\check{p}_{k}}$), we can now show: $(\check{r}=\check{u}/\check{i})\Leftrightarrow(\check{r}=\check{r}_{1}+\check{r}_{2})$ since $\forall k\in\{1,2\}:\check{r}_{k}={\check{u}_{k}/\check{i}_{k}}$, ${\check{i}_{1}=\check{i}_{2}}$ and $\check{u}={\check{u}_{1}+\check{u}_{2}}$. Similarly, we can show: $\check{\mathcal{P}}={\check{\mathcal{P}}_{1}+\check{\mathcal{P}}_{2}}$ for the power dissipation (defined as $\mathcal{P}=u\cdot i$) or $\check{r}=(1/\check{r}_{1}+1/\check{r}_{2})^{-1}$ for parallel composition of resistors.

As we explained in the preliminaries, contracts are interpreted by tuples $(\mathcal{E},\mathcal{M})$ of subsets of $\mathbb{M}$. Thus, two semantically different, valid assertions $G_{1}\!\neq\!G_{2}$ must be interpreted to two different subsets $\mathcal{M}_{1}\!\neq\!\mathcal{M}_{2}\!\subset\!\mathbb{M}$. Vice versa: to distinguish two different (sets of) components $\mathcal{M}_{1}\!\neq\!\mathcal{M}_{2}\!\subset\!\mathbb{M}$ by contracts $(A,G)$, the syntax and the semantics of $A$ and $G$ must be able to describe and reflect the specific distinction. Thus, if a difference in the composition operation is relevant for the validity of composing contracts (and checking their refinement), the assumptions and guarantees must be able to catch this. For our example, if we want a valid serial decomposition of $\check{r}$, it would not be sufficient to specify only a value (e. g. $\check{r}\!=\!3$) for the resistance, since – e. g. having subcomponents $\check{M}_{1},\check{M}_{2}$ with $\check{r}_{1}\!=\!1$ and $\check{r}_{2}\!=\!2$ – there are several composition operations which erroneously would satisfy $\check{r}\!=\!3$, e. g. $\check{r}=3\check{r}_{1}\!+\!0\check{r}_{2}$ While those composition operations have same type signatures $\mathbb{M}\!\times\!\mathbb{M}\!\rightarrow\!\mathbb{M}$, mapping $n\!=\!2$ resistors $\check{M}_{k}\!\in\!\mathbb{M}$ to a resistor $\check{M}\!\in\!\mathbb{M}$ their term signatures (e. g. $3\check{r}_{1}\!+\!0\check{r}_{2}\not\equiv\check{r}_{1}+\check{r}_{2}$) differ.

However, in the definition of the composition operation $\otimes^{\mathbb{C}}_{k\in K_{n}}$ for contracts (cf. preliminaries), CBD requires a contract theory to provide a fixed composition operation $\otimes^{\mathbb{M}}_{k\in K_{n}}$, whose type and term signature is valid for all $\check{M}^{*}\in\mathbb{M}^{n}$. This limits the applicability of contract based design to components, which do not need to distinguish their properties by means of the composition term. As a consequence, a contract theory can support correct composition (and thus refinement checking) for only a limited number of $s\in\mathbb{N}$ predefined component subsets $\mathbb{M}_{k\in K_{s}}\subseteq\mathbb{M}$ with $\bigcap_{\forall k\in K_{s}}\mathbb{M}_{k}=\varnothing$ and $\bigcup_{\forall k\in K_{s}}\mathbb{M}_{k}=\mathbb{M}$.

Related Work.

As we first identified the difficulties with properly defining, composing and refining EFPs in terms of contracts, we outlined a problem sketch in [2] and suggested an early approach, based on extending the refining set $\check{M}^{*}$ by another subcomponent, having assumptions and guarantees about the interconnection relations between the other components’ variables. Most closely related, [4] agrees with our idea, but by distinguishing different contract types and specifying assertion and validity rules (i. e. functions and predicates) between the variables of that contract types. In contrast to SCs, these rules and types are defined as sets at the level of platforms, limiting the set of correctly refineable property specifications according to only those rules and types of that platform. Being based on the concept of type constructors and product types, we belief our SCs to be a more generic approach that is able to express required type and composition constraints also between different platforms and to support their bidirectional propagation across multiple levels of hierarchical composition. Furthermore, vertical contracts [3] propose an architecture mapping relation to relate aggregation functions between the two hierarchy levels of a refinement. However, their aggregation function captures only parallel and conjunctive composition $\otimes^{\mathbb{C}}_{k}$ and $\land^{\mathbb{C}}_{k}$ of contracts. Further related work investigates e. g.: (meta)-model-based composition rules for composing EFPs via contracts [5]; consistency reasoning for contracts based on onthologies [7]; or Galois Connections for the compositional abstraction of contracts [1].

0.0.3 Our Approach of Structural Contracts.

To allow CBD to correctly reason about an arbitrary number of user-defined (extra-functional) properties, our goal is to extend CBD by a specification and verification mechanism – called structural contracts (SCs) – that constrains the accepted term and type signatures of component construction and composition, which means: a) allowing to control the partitioning of $\mathbb{M}$ into a set $\mathbb{M}_{S}\Coloneqq\bigcup_{\forall k\in K_{s}}\{\mathbb{M}_{k}\}$ of $s$ hierarchically ordered, (extra-functional) subdomains $\mathbb{M}_{k}$, and b) allowing to specify the composition operations $\otimes^{\mathbb{M}_{S}}_{k\in K_{n}}$, whose type signatures are defined via the product type $\Pi_{\forall k\in K_{n},\forall\mathbb{M}_{k}\in\mathbb{M}_{S}}\mathbb{M}_{k}\rightarrow\check{\mathbb{M}}\in\mathbb{M}_{S}$. Thus, following the Curry-Howard-Isomorphism of ‘propositions-as-types’ [6] from constructive type theory, a similarly comprehensive ‘structural’ notion of contracts (‘contracts-as-types’) requires several extensions w. r. t. polymorphic and dependent types:

language extension of contracts, to allow for a specification of polymorphic and dependent type requirements (i. e. the syntax of our SCs); 2. 2.

semantical extension from a set $\mathbb{M}$ of components to a hierarchically ordered, extensible set of component-types $\mathbb{M}_{k}\!\in\!\mathbb{M}_{S}$, based on type- & term-dependent type-constructors (i. e. the type-theoretic semantics of our SCs); 3. 3.

implement and integrate algorithms for the corresponding type checking;

For brevity, we here focus only on giving an outline of point 2: To enable polymorphic and dependent product types for contracts, we must be able to overload the composition operation $\otimes^{\mathbb{M}_{S}}_{k}$ with an appropriate, user definable term signature for each type signature of the product type $\Pi_{\forall k\in K_{n},\forall\mathbb{M}_{k}\in\mathbb{M}_{S}}\mathbb{M}_{k}$.

For our example, this would mean the declaration of the type ‘resistance’ as $\mathbb{M}_{r}:\bot\rightarrow\mathbb{M}$, which can be used for the generation of the type ’resistor’ $\mathbb{M}_{M_{r}}:\mathbb{M}_{r}\rightarrow\mathbb{M}$, i. e. components with a property $r$ of type $\mathbb{M}_{r}$ denoted by $r:\mathbb{M}_{r}$. With that, the type signature of our composition operation can become $\otimes^{\mathbb{M}_{r}}:(\mathbb{M}_{r}\times\mathbb{M}_{r})\rightarrow\mathbb{M}_{r}$ or generally $\otimes^{\mathbb{M}_{r}}:(\Pi_{k\in\mathbb{N}}\mathbb{M}_{r}^{k})\rightarrow\mathbb{M}_{r}$. Furthermore, to define new (sub-)types within the type hierarchy of $\mathbb{M}_{S}$, we suggest to have type constructors $\mathbb{M}_{k}:\bot\rightarrow\mathbb{M}_{S}\cup\{\mathbb{M}_{S}\}$, meaning the declaration of the type $\mathbb{M}_{k}$ as a base type in $\mathbb{M}_{S}$ or as a subtype of some other $\mathbb{M}_{k^{\prime}}\in\mathbb{M}_{S}$.

0.0.4 Status and Future Work.

Investigating CBD for EFPs, we identified difficulties w. r. t. the ability to specify user-defined property-domains and composition operations. As a promising approach, we now combine CBD with dependent types and constraints for the type constructors. After finishing the theoretic fundament and a first implementation, we plan to evaluate our SCs for different EFPs of embedded, electrical systems, like timing, power consumption and heating.