key: cord-0059306-ijyfzghm
authors: Lidström, Christian; Gurov, Dilian
title: An Abstract Contract Theory for Programs with Procedures
date: 2021-02-24
journal: Fundamental Approaches to Software Engineering
DOI: 10.1007/978-3-030-71500-7_8
sha: 878fe008ad22db3e24216455dae235736bd0f251
doc_id: 59306
cord_uid: ijyfzghm

When developing complex software and systems, contracts provide a means for controlling the complexity by dividing the responsibilities among the components of the system in a hierarchical fashion. In specific application areas, dedicated contract theories formalise the notion of contract and the operations on contracts in a manner that supports best the development of systems in that area. At the other end, contract meta-theories attempt to provide a systematic view on the various contract theories by axiomatising their desired properties. However, there exists a noticeable gap between the most well-known contract meta-theory of Benveniste et al. [5], which focuses on the design of embedded and cyber-physical systems, and the established way of using contracts when developing general software, following Meyer’s design-by-contract methodology [18]. At the core of this gap appears to be the notion of procedure: while it is a central unit of composition in software development, the meta-theory does not suggest an obvious way of treating procedures as components. In this paper, we provide a first step towards a contract theory that takes procedures as the basic building block, and is at the same time an instantiation of the meta-theory. To this end, we propose an abstract contract theory for sequential programming languages with procedures, based on denotational semantics. We show that, on the one hand, the specification of contracts of procedures in Hoare logic, and their procedure-modular verification, can be cast naturally in the framework of our abstract contract theory. On the other hand, we also show our contract theory to fulfil the axioms of the meta-theory. In this way, we give further evidence for the utility of the meta-theory, and prepare the ground for combining our instantiation with other, already existing instantiations.

Contracts. Loosely speaking, a contract for a software or system component is a means of specifying that the component obliges itself to guarantee a certain behaviour or result, provided that the user (or client) of the component obliges itself to fulfil certain constraints on how it interacts with the component. dure is a central unit of composition in software development, the meta-theory does not suggest an obvious way of treating procedures as components. This situation is not fully satisfactory, since the software components of most embedded systems are implemented with the help of procedures (a typical C-module, for instance, would consist of a main function and a number of helper functions), and their development should ideally follow the same design flow as that of the embedded system as a whole.

In this paper we provide a first step towards a contract theory that takes procedures as the basic building block, and at the same time respects the axioms of the meta-theory. Our contract theory is abstract, so that it can be instantiated to any procedural language, and similarly to the meta-theory, is presented at the semantics level only. Then, in the context of a simplistic imperative programming language with procedures and its denotational semantics, we show that the specification of contracts of procedures in Hoare logic, and their procedure-modular verification, can be cast in the framework of our abstract contract theory. We also show that our contract theory is an instance of the meta-theory of Benveniste et al. With this we expect to contribute to the bridging of the gap mentioned above, and to give a formal justification of the design methodology supported by the meta-theory, when applied to the software components of embedded systems. Several existing contract theories have already been shown to instantiate the meta-theory. In providing a contract theory for procedural programs that also instantiates it, we increase the value of the metatheory by providing further evidence for its universality. In addition, we prepare the theoretical ground for combining our instantiation with other instantiations, which may target components not to be implemented in software.

Our theoretical development should be seen as a proof-of-concept. In future work it will need to be extended to cover more programming language features, such as object orientation, multi-threading, and exceptions.

Related Work. Software contracts and operations on contracts have long been an area of intensive research, as evidenced, e.g., by [1] . We briefly mention some works related to our theory, in addition to the already mentioned ones.

Reasoning from multiple Hoare triples is studied in [21] , in the context of unavailable source code, where new properties cannot be derived by re-verification. In particular, it is found that two Hoare-style rules, the standard rule of consequence and a generalised normalisation rule, are sufficient to infer, from a set of existing contracts for a procedure, any contract that is semantically entailed.

Often-changing source code is a problem for contract-based reasoning and contract reuse. In [13] , abstract method calls are introduced to alleviate this problem. Fully abstract contracts are then introduced in [7] , allowing reasoning about software to be decoupled from contract applicability checks, in a way that not all verification effort is invalidated by changes in a specification.

The relation between behavioural specifications and assume/guarantee-style contracts for modal transition systems is studied in [2] , which shows how to build a contract framework from any specification theory supporting composition and refinement. This work is built on in [9] , where a formal contract framework based on temporal logic is presented, allowing verification of correctness of contract refinement relative to a specific decomposition.

A survey of behavioural specification languages [14] found that existing languages are well-suited for expressing properties of software components, but it is a challenge to express how components interact, making it difficult to reason about system and architectural level properties from detailed design specifications. This provides additional evidence for the gap between contracts used in software verification and contracts as used in system design.

Structure. The paper is organised as follows. Section 2 recalls the concept of contract based design and the contract meta-theory considered in the present paper. In Section 3 we present a denotational semantics for programs with procedures, including a semantics for contracts for use in procedure-modular verification. Next, Section 4 presents our abstract contract theory for sequential programs with procedures. Then, we show in Section 5 that our contract theory fulfils the axioms of the meta-theory, while in Section 6 we show how the specification of contracts of procedures in Hoare logic and their procedure-modular verification can be cast in the framework of our abstract contract theory. We conclude with Section 7.

This section describes the concept of contract based design, and motivates its use in cyber-physical systems development. We then recall the contract meta-theory by Benveniste et al. [5] .

Contract based design is an approach to systems design, where the system is developed in a top-down manner through the use of contracts for components, which are incrementally assembled so that they preserve the desired system-wide properties. Contracts are typically described by a set of assumptions the component makes on its environment, and a set of guarantees on the component's behaviour, given that it operates in an environment adhering to the assumptions [5] .

Present-day cyber-physical systems, such as those found in the automotive, avionics and other industries, are extremely complex. Products assembled by Original Equipment Manufacturers (OEMs) often consist of components from a number of different suppliers, all using their own specialised design processes, system architectures, development platforms, and tools. This is also true inside the OEMs, where there are different teams with different viewpoints of the system, and their own design processes and tools. In addition, the system itself has several different aspects that need to be managed, such as the architecture, safety and security requirements, functional behaviour, and so on. Thus, a rigorous design framework is called for that can solve these design-chain management issues.

Contract based design addresses these challenges through the principles, at the specification level, of refinement and abstraction, which are processes for managing the design flow between different layers of abstraction, and composition and decomposition, which manage the flow at the same level of abstraction. Generally, when designing a system, at the top level of abstraction there will be an overall system specification (or contract). This top-level contract is then refined, to provide a more concrete contract for the system, and decomposed, in order to obtain contracts for the sub-systems, and to separate the different viewpoints of the system. A system design typically iterates the decompositionand-refinement process, resulting in several layers of abstraction, until contracts are obtained that can be directly implemented, or for which implementations already exist. An important requirement on this methodology of hierarchical decomposition and refinement of contracts is that it must guarantee that when the low-level components implement their concrete contracts, and are combined to form the overall system, then the top-level, abstract, contract shall hold.

Furthermore, a contract framework in particular needs to support independent development and component reuse. That is, specifications for components, and their operations, must allow for components and specifications to be independently designed and implemented, and to be used in different parts of the system, each with their own assumptions on how the other components, the environment, behave. This is achieved through the principle operations on contracts: refinement, composition, and conjunction.

Refinement allows one to extract a contract at the appropriate level of abstraction. A desired property of refinement is that components which have been designed with reference to the more abstract (i.e., weaker) contract do not need to be re-designed after the refinement step. That is, in the early stages of development an OEM may have provided a weak contract for some subsystem to an external supplier, which implemented a component relying on this contract. As development of the system progresses, and the contract is refined, the component supplied externally should still operate according to its guarantees without needing to be changed, when instead assuming the new, refined, contract.

Composition enables one to combine contracts of different components into a contract for the larger subsystem obtained when combining the components. Again, a desirable property is that other components relying on one or more of the individual contracts, can, after composition of the contracts, assume the new contract and still perform its guarantees, without being re-designed, thus ensuring that subsystems can be independently implemented.

Finally, contract conjunction is another way of combining contracts, but now for the different viewpoints of a single component. This allows one to separate a contract into several different, finer contracts for the same component, revealing just enough information for each particular system that depends on it, so that it can be reused in different parts of the system, or in entirely different systems.

We consider the meta-theory described in [5] . The stated purpose of the metatheory has been to distil the notion of a contract to its essence, so that it can be used in system design methodologies without ambiguities. In particular, the meta-theory has been developed to give support for design-chain management, and to allow component reuse and independent development. It has been shown that a number of concrete contract theories instantiate it, including assume/guarantee-contracts, synchronous Moore interfaces, and interface theories. To our knowledge, this is the only meta-theory of its purpose and scope.

We now present the formal definitions of the concepts defined in the metatheory, and the properties that they entail. The meta-theory is defined only in terms of semantics, and it is up to particular concrete instantiations to provide a syntax.

Components. The most basic concept in the meta-theory is that of a component, which represents any concrete part of the system. Thus, we have an abstract component universe M with components m ∈ M. Over pairs of components, we have a composition operation ×. This operation is partially defined, and two components m 1 and m 2 are called composable when m 1 × m 2 is defined. In such cases, we call m 1 an environment for m 2 , and vice versa. In addition, component composition must be both commutative and associative, in order to ensure that different components can be combined in any order.

Typically, components are open, in the sense that they contain functionality provided by other components, i.e., their environment. The environment in which a component is to be placed is often unknown at development time, and although a component cannot restrict it, it is designed for a certain context.

In the meta-theory, the notion of contract is defined in terms of sets of components. The contract universe C def = 2 M × 2 M consists of contracts C = (E, M ), where E and M are the sets of environments and implementations of C, respectively. Importantly, each pair (m 1 , m 2 ) ∈ E ×M must be composable. This definition is intentionally abstract. The intuition is that contracts separate the responsibilities of a component from the expectations on its environment. Moreover, contracts are best seen as weak specifications of components: they should expose just enough information to be adequate for their purpose.

For a component m and a contract C = (E, M ), we shall sometimes write m |= E C for m ∈ E, and m |= M C for m ∈ M . A contract C is said to be consistent if it has at least one implementation, and compatible if it has at least one environment.

As an axiom of the meta-theory, it is required that the greatest lower bound with respect to refinement exists, for all subsets of C. Table 1 summarises the important properties of refinement and the other operations on contracts that a concrete Refinement. When C1 C2, every implementation of C1 is also an implementation of C2.

2 Shared refinement. Any contract refining C1 ∧ C2 also refines C1 and C2. Any implementation of C1 ∧ C2 is a shared implementation of C1 and C2. Any environment for C1 and C2 is an environment for C1 ∧ C2.

3 Independent implementability. Compatible contracts can be independently implemented.

4

Independent refinement. For all contracts Ci and

Commutativity, sub-associativity. For any finite sets of contracts Ci, i = 1, . . . , n, C1 ⊗ C2 = C2 ⊗ C1 and 1≤i≤n Ci ( 1≤i<n Ci) ⊗ Cn holds.

6

Sub-distributivity. The following holds, if all contract compositions in the formula are well defined:

contract theory needs to possess in order to be considered an instance of the meta-theory.

Contract conjunction. The conjunction of two contracts C 1 and C 2 , denoted

; however, this cannot be taken as the definition since not every such pair necessarily constitutes a contract.) Then, we have the three desirable properties of conjunction listed in Table 1 , which together are referred to as shared refinement.

Contract composition. The composition of two contracts C 1 = (E 1 , M 1 ) and

, is defined when every two components m 1 ∈ M 1 and m 2 ∈ M 2 are composable, and must then be the least contract, w.r.t. the refinement order, satisfying the following conditions:

If all of the above is satisfied, then properties 3-6 of Table 1 hold. The intention is that composing two components implementing C 1 and C 2 should yield an implementation of C 1 ⊗ C 2 , and composing an environment of C 1 ⊗ C 2 with an implementation of C 1 should result in a valid environment for C 2 , and vice versa. This is important in order to enable independent development.

In this section we summarise the background needed to understand the formal developments later in the paper. First, we recall the standard denotational semantics of programs with procedures on a typical toy programming language.

Next, we summarise Hoare logic and contracts, and provide a semantic justification of procedure-modular verification, also based on denotational semantics.

This section sketches the standard presentation of denotational semantics for procedural languages, as presented in textbooks such as [23, 19] . This semantics is the inspiration for the definition of components in our abstract contract theory in Section 4.1. We start with a simplistic programming language not involving procedures, and add procedures later to the language.

The following toy sequential programming language is typically used to present the denotational semantics of imperative languages:

where S ranges over statements, a over arithmetic expressions, and b over Boolean expressions.

To define the denotational semantics of the language, we define the set State of program states. A state s ∈ State is a mapping from the program variables to, for simplicity, the set of integers.

The 

For the treatment of the remaining statements of the language, the reader is referred to [23, 19] .

The definition of denotation captures through its type (as a partial function) that the execution of statements is deterministic. For non-deterministic programs, the type of denotations is relaxed to

captures that there is an execution of S starting in s that terminates in s . For technical reasons that will become clear below, we shall use this latter denotation type in our treatment.

Note that we could alternatively have chosen State + as the denotational domain, and most results would still hold in the context of finite-trace semantics. However, we chose to develop the theory with a focus on Hoare-logic and deductive verification. In fact, the domain State × State can be seen as a special case of finite traces. In future work, we will also investigate concrete contract languages based on this semantics, and extend the theory for that context.

Procedures and Procedure Calls. To extend the language and its denotational semantics with procedures and procedure calls, we follow again the approach of [23] , but adapt it to an "open" setting, where some called procedures might not be declared. We consider programs in the context of a finite set P of procedure names (of some larger, "closed" program), and a set of procedure declarations of the form proc p is S p , where p ∈ P. Further, we extend the toy programming language with the statement call p. Listing 1.1. An even-odd toy program. proc even i s i f n = 0 then r := 1 e l s e ( n := n − 1 ; c a l l odd ) ; proc odd i s i f n = 0 then r := 0 e l s e ( n := n − 1 ; c a l l even )

As an example, Listing 1.1 shows a (closed) program in the toy language, implementing two mutually recursive procedures. The procedures check whether the value of the global variable n is even or odd, respectively, and assign the corresponding truth value to the variable r.

Due to the (potential) recursion in the procedure declarations, the denotation of call p, and thus of the whole language, cannot be defined by structural induction as directly as before. We therefore define, for any set P ⊆ P of procedure names, the set Env P = P → 2 State×State of procedure environments, each environment ρ ∈ Env P thus providing a denotation for each procedure in P .

Let Env def = P ⊆P Env P be the set of all procedure environments. We define a partial order relation on procedure environments, as follows. For any two procedure environments ρ ∈ Env P and ρ ∈ Env P , ρ ρ if and only if P ⊆ P and ∀p ∈ P. ρ(p) ⊆ ρ (p).

Recall that a complete lattice is a partial order, every set of elements of which has a greatest lower bound (glb) within the domain of the lattice (see, e.g., [23] ). It is easy to show that for any P ⊆ P, (Env P , ) is a complete lattice, since a greatest lower bound will exist within Env P . Then, the least upper bound (lub) ρ 1 ρ 2 of any two function environments ρ 1 ∈ Env P1 and ρ 2 ∈ Env P2 also exists, and is the environment ρ ∈ Env P1∪P2 such that ∀p ∈ P 1 ∪P 2 . ρ(p) = ρ 1 (p)∪ρ 2 (p).

We will sometimes need a procedure environment that maps every procedure in P to State × State, and we shall denote this environment by ρ P .

Next, for sets of procedures, we shall need the notion of interface, which is a pair (P − , P + ) of disjoint sets of procedure names, where P + ⊆ P is a set of provided (or declared) procedures, and P − ⊆ P a set of required (or called, but not declared) ones.

Then, we (re)define the notion of denotation of statements S in the context of a given interface (P − , P + ) and environments ρ − ∈ Env P − and ρ + ∈ Env P + , and denote it by

Intuitively, the denotation of a call to a procedure should be equal to the denotation of the body of the latter. We therefore introduce, given an environment ρ − ∈ Env P − , the function ξ : Env

for any ρ + ∈ Env P + and p ∈ P + , and consider its fixed points. By the Knaster-Tarski Fixed-Point Theorem (as stated, e.g., in [23] ), since (Env P + , ) is a complete lattice and ξ is monotonic, ξ has a least fixed-point ρ + 0 .

Finally, we define the notion of standard denotation of statement S in the context of a given interface (P − , P + ) and environment ρ − ∈ Env P − , denoted 

In this section we summarise the denotational semantics of Hoare logic and the semantic justification of procedure-modular verification, as developed by the second author in [12] . These formalisations serve as the starting point for the definition of contracts in our contract theory developed in Section 4.2.

Hoare Logic. The basic judgement of Hoare logic [15] is the Hoare triple, written {P }S{Q}, where P and Q are assertions over the program state, and S is a program statement. The Hoare triple signifies that if the statement S is executed from a state that satisfies P (called the pre-condition), and if this execution terminates, then the final state of the execution will satisfy Q (called the postcondition). Additionally, so-called logical variables can be used within a Hoare triple, to specify the desired relationship between the values of variables after execution and the values of variables before execution. The values of the program variables are defined by the notion of state; to give a meaning to the logical variables we shall use interpretations I. We shall write s |= I P to signify that the assertion P is true w.r.t. state s and interpretation I. The formal validity of a Hoare triple is denoted by |= par {P }S{Q}, where the subscript signifies that validity is in terms of partial correctness, where termination of the execution of S is not required.

An example of a Hoare triple, stating the desired behaviour of procedure odd from Listing 1.1, is shown below, where we use the logical variable n 0 to capture to the value of n prior to execution of odd :

Procedure even is specified analogously.

Hoare logic comes with a proof calculus for reasoning in terms of Hoare triples, consisting of proof rules for the different types of statements of the programming language. An example is the rule for sequential composition:

Composition which essentially states that if executing S 1 from any state satisfying P terminates (if at all) in some state satisfying R, and executing S 2 from any state satisfying R terminates (if at all) in some state satisfying Q, then it is the case that executing the composition S 1 ; S 2 from any state satisfying P terminates (if at all) in some state satisfying Q. The proof system is sound and relatively complete w.r.t. the denotational semantics of the programming language (see, e.g., [23, 19] ).

Hoare Logic Contracts. One can view a Hoare triple {P }S{Q} as a contract C = (P, Q) imposed on the program S. In many contexts it is meaningful to separate the contract from the program; for instance, if the program is yet to be implemented. In our earlier work [12] , we gave such contracts a denotational semantics as follows:

The rationale behind this definition is the following desirable property: a program meets a contract whenever its denotation is subsumed by the denotation of the contract, i. The Denotational Semantics of Programs with Procedure Contracts. Let S be a program with procedures, and let every declared procedure p ∈ P be equipped with a procedure contract C p . Procedure-modular verification refers to techniques that verify every procedure in isolation. The key to this is to handle procedure calls by using the contract of the called procedure rather than its body (i.e., by contracting rather than by inlining [7] ). In [12] , a semantic justification of this is given by means of a contract-relative denotational semantics of statements. The intuition behind this semantics is that procedure calls are given a meaning through the denotation of the contract of the called procedure, rather than through the denotation of its body.

The contract-relative denotational semantics of a statement S, denoted [[S]] cr , is defined with the help of the contract environment ρ c that is induced by the procedure contracts, i.e., ρ c (p) ]. This is exactly the correctness notion that is the target of procedure-modular verification. As shown in [12] , this notion is sound w.r.t. the original notion S |= par C, in the sense that S |= cr par C entails S |= par C. In other words, verifying a program procedure-modularly establishes that the program is correct w.r.t. its contract in the standard sense.

For example, the contract-relative semantics of S even is such that (s, s ) ∈ if s(n) is even and s (r) = 0 if s(n) is odd. The contract-relative semantics of S odd is analogous. Then, it is easy to check that both S even |= cr par C even and S odd |= cr par C odd hold.

This section presents an abstract contract theory for programs with procedures. The theory builds on the basic notion of denotation as a binary relation over states. As we will show later, it is both an abstraction of the denotational semantic view on programs with procedures and procedure contracts presented in Sections 3.1 and 3.2, and an instantiation of the meta-theory described in Section 2.2.

In the context of a concrete programming language, we view a component as a module, consisting of a collection of procedures that are provided by the module. The module may call required procedures that are external to the module. The way the provided procedures transform the program state upon a call depends on how the required procedures transform the state. We take this observation as the basis of our abstract setting, in which state transformers are modelled as denotations (i.e., as binary relations over states). A component will thus be simply a mapping from denotations of the required procedures to denotations of the provided ones, both captured through the notion of procedure environments. The contract theory is abstract, in that it is not defined for a particular programming language, and may be instantiated with any procedural language. As with the meta-theory, the abstract contract theory is also defined only on the semantic level.

Recall the notions and notation from Section 3.1. A component interface I = (P − , P + ) is a pair of disjoint, finite sets of procedure names, of the required and the provided ones, respectively.

Let M denote the universe of all components over P.

We assume that any system is built up from a set of base components, the simplest components from which more complex components are then obtained by composition. The base components must be monotonic functions over the lattice defined in Section 3.1.

When P − m = ∅, we shall identify m with an element of Env P + m . In other words, when a component is closed, i.e., is not dependent on any external procedures, the provided environment is constant.

Definition 2 (Component composability). Two components m 1 and m 2 are composable iff P + m1 ∩ P + m2 = ∅.

When defining the composition of two components, particular care is required in the treatment of procedure names that are provided by one of the components while required by the other. Let μx. f (x) denote the least fixed-point of a function f , when it exists.

, their composition is defined as a mapping m 1 × m 2 : Env P − m 1 ×m 2 → Env P + m 1 ×m 2 such that:

is defined, in the context of a given

be defined symmetrically. We then define:

In the above definition, χ + m1×m2 represents the denotations of the procedure bodies of the procedures provided by the two composed components, given denotations of procedure calls to the same procedures. The choice of least fixed-point will be crucial for the proof of Theorem 2(i) in Section 4.2 below.

The definition is well-defined, in the sense that the stated least fixed-points exist, and the resulting components are monotonic functions.

The existence of a least fixed-point follows from the Knaster-Tarski Fixed-Point Theorem, as stated, e.g., in [23] . It can then be shown, by structural induction, that composition is well-defined. For lack of space, the proofs of all theorems, some of which are conceptually not very involved but rather verbose, are omitted here. The full proofs can be found in the accompanying technical report [17] .

We now define the notion of denotational contracts c in the style of assume/guarantee contracts [4, 6] . Contracts shall also be given interfaces.

and ρ + c ∈ Env P + c . The intended interpretation of the environment pair is as follows: assuming that the denotation of every called procedure p ∈ P − c is subsumed by ρ − c (p), then it is guaranteed that the denotation of every provided procedure p ∈ P + c is subsumed by ρ + c (p ).

The reason for not requiring the interfaces to be equal is that we aim at a subset relation between components implementing a contract and those implementing a refinement of said contract, in the meta-theory instantiation. 

Intuitively, an environment of a contract c is then a component such that when it is composed with an implementation of c, the composition will operate satisfactorily with respect to the guarantee of the contract. We will now define the refinement relation, and the conjunction and composition operations, on contracts. The refinement relation reflects the intention that if a contract c refines another contract c , then any component implementing c should also implement c . This definition is consistent with the intention that any contract that refines c 1 ∧ c 2 should also refine c 1 and c 2 individually. The interface of c 1 ∧ c 2 is then

. Note that while this is the interface in general, conjunction of contracts is typically used to merge different viewpoints of the same component, and in that case I c1 = I c2 = I c1∧c2 .

Definition 9 (Contract composability). Two contracts c 1 = (ρ − c1 , ρ + c1 ) and c 2 = (ρ − c2 , ρ + c2 ) with interfaces I c1 = (P − c1 , P + c1 ) and I c2 = (P − c2 , P + c2 ) are composable if:

The conditions for composability ensure that the mutual guarantees of the two contracts meet each other's assumptions.

Definition 10 (Contract composition). The composition of two composable contracts c 1 = (ρ − c1 , ρ + c1 ) and c 2 = (ρ − c2 , ρ + c2 ), with interfaces I c1 = (P − c1 , P + c1 ) and

For any composable contracts c 1 and c 2 , and any implementations m 1 |= c 1 and m 2 |= c 2 , m 1 and m 2 are composable, and c 1 ⊗ c 2 is the least contract (w.r.t. refinement order) for which the following properties hold:

In this section we show that the abstract contract theory presented in Section 4 instantiates the meta-theory described in Section 2.2.

In our instantiation of the meta-theory, we consider as the abstract component universe M the same universe of components M as defined in Section 4.1.

To distinguish the contracts of the meta-theory from those of the abstract theory, we shall always denote the former by C and the latter by c. Recall that a contract C is a pair (E, M ), where E, M ⊆ M. The formal connection between the two notions is established with the following definition. Since contract implementation requires that the implementing component's provided functions are a subset of the contract's provided functions, every component m such that P + m ∩ P + c = ∅ is composable with every component in M c . The definitions of implementation, refinement and conjunction of denotational contracts make this straightforward definition of induced contracts possible, so that it directly results in refinement as set membership and conjunction as lub w.r.t. the refinement order.

Theorem 3. The contract theory of Section 4 instantiates the meta-theory of Benveniste et al. [5] , in the sense that composition of components is associative and commutative, and for any two contracts c 1 and c 2 :

(i) c 1 c 2 iff C c1 refines C c2 according to the definition of the meta-theory, (ii) C c1∧c2 is the conjunction of C c1 and C c2 as defined in the meta-theory, and (iii) C c1⊗c2 is the composition of C c1 and C c2 as defined in the meta-theory.

The proof is straightforward, since many definitions of the contract theory are deliberately similar to their counterparts in the meta-theory.

Let us now return to our example from Section 3. When applying Contract Based Design, contracts at the more abstract level will be decomposed into contracts at the more concrete level. So, for our example, we might have at the top level a contract c = (ρ − c , ρ + c ) with interface (∅, {even, odd}) , where ρ − c = ∅, and where ρ + c ∈ Env P + c maps even to the set of pairs (s, s ) such that whenever s(n) is non-negative and even, then s (r) = 1, and when s(n) is non-negative and odd, then s (r) = 0, and maps odd in a dual manner. This contract could then be decomposed into two contracts c even and c odd , so that ρ + ceven (even) def = ρ + c (even) and ρ − ceven (odd ) def = ρ + c (odd ), and c odd is analogous. Then, we would have c even ⊗ c odd c, and for any two components m even and m odd such that m even |= c even and m odd |= c odd , it would hold that m even × m odd |= c.

In this section we discuss how our abstract contract theory from Section 4 relates to programs with procedures as presented in Section 3.1, and how it relates to Hoare logic and procedure-modular verification as presented in Section 3.2.

First, we define how to abstract the denotational notion of procedures into components in the abstract theory, based on the function ξ from Section 3.1.

Definition 12 (From procedure sets to components). For any set of procedures P + , calling procedures P , we define the component m :

As the next result shows, procedure set abstraction and component composition commute. Together with commutativity and associativity of component composition, this means that the initial grouping of procedures into components is irrelevant, and that one can start with abstracting each individual procedure into a component. The result is a direct consequence of Definition 12, Definition 3, and the well-known Bekić's Lemma [3] about simultaneous fixed-points. ρ + = ξ(ρ + )(even). Similarly χ + meven ×m odd (ρ + )(odd ) = ξ(ρ + )(odd ). We therefore have m even × m odd = m.

We now define how to abstract Hoare logic contracts into denotational contracts, in terms of the contract environment ρ c defined in Section 3.2. In this way, conceptually, denotational contracts become assume/guaranteestyle specifications over Hoare logic procedure contracts: assuming that all (ex-ternal) procedures called by a procedure p transform the state according to their Hoare logic contracts, procedure p obliges itself to do so as well.

We now show that if a procedure implements a Hoare logic contract, then the abstracted component will implement the abstracted contract, and vice versa. Together with Theorem 4, this result allows the procedure-modular verification of abstract components.

Theorem 5. For any procedure p with procedure contract C p , abstracted into component m p with contract c p , we have S p |= cr par C p iff m p |= c p .

The result follows mainly from Definitions 12 and 13, and the denotational semantics given in Section 3.

Returning to the example from Sections 3 and 5, we can abstract the procedure set {even} into component m even , with interface ({odd}, {even}), which would be a function Env {odd} → Env {even} , and ∀ρ − ∈ Env {odd} . m(ρ − )(even) = [[S even ]] ρ − . The denotational contracts c even and c odd resulting from the decomposition shown in Section 5, would be exactly the abstraction of the Hoare Logic contracts C even and C odd shown in Section 3.2. They would both be part of the contract environment used in procedure-modular verification, for example when verifying that S even |= cr par C even , which would entail m even |= c even . Thus, by applying standard procedure-modular verification at the source code level, we prove the top-level contract c proposed in Section 5.

We presented an abstract contract theory for procedural languages, based on denotational semantics. The theory is shown to be an instance of the meta-theory of [5] , and at the same time an abstraction of the standard denotational semantics of procedural languages. We believe that our contract theory can be used to support the development of cyber-physical and embedded systems by the design methodology supported by the meta-theory, allowing the individual procedures of the embedded software to be treated as any other system component. The work also strengthens the claims of the meta-theory of distilling the notion of contracts to its essence, by showing that it is applicable also in the context of procedural programs and deductive verification. Finally, this work serves as a preparation for combining our contract theory for procedural programs with other instantiations of the meta-theory. In future work we plan to investigate the utility of our contract theory on real embedded systems taken from the automotive industry, where not all components are procedural programs, or even software (cf. our previous work, e.g., [11] ). We also plan to extend our toy imperative language with additional features, such as procedure parameters and return values. Furthermore, we plan to extend the contract theory to capture program traces by developing a finite-trace semantics, to enable its use in the specification and verification of temporal properties. Lastly, we plan to combine our contract theory with an existing contract theory for hybrid systems [20] .

Composing specifications

Moving from specifications to contracts in component-based design

Definable operation in general algebras, and the theory of automata and flowcharts

Multiple viewpoint contract-based specification and design

Contracts for System Design

A contract-based formalism for the specification of heterogeneous systems

Fully abstract operation contracts

A compositional specification theory for component behaviours

Contracts-refinement proof system for componentbased embedded systems

Assigning meanings to programs

Deductive functional verification of safety-critical embedded c-code: An experience report

A Hoare Logic Contract Theory: An Exercise in Denotational Semantics

Reuse in software verification by abstract method calls

Behavioral interface specification languages

An axiomatic basis for computer programming

Specification and design of (parallel) programs

An abstract contract theory for programs with procedures (full version)

Applying "design by contract"

Semantics with Applications: An Appetizer

Formally proving compositionality in industrial systems with informal specifications

Hoare-style reasoning from multiple contracts

On rely-guarantee reasoning

The Formal Semantics of Programming Languages: An Introduction

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use