Cosimo Laneve

Luca Padovani

Under consideration for publication in Formal Aspects of Computing An Algebraic Theory for Web Service Contracts

Keywords: Web services, bpel, contracts, compliance, must-testing, coinductive subcontract, dual contract, choreography

come   L'archive ouverte pluridisciplinaire

Introduction

Service-oriented technologies and Web services have been proposed as a new way of distributing and organizing complex applications across the Internet. These technologies are nowadays extensively used for delivering cloud computing platforms. A large effort in the development of Web services has been devoted to their specification, their publication, and their use. In this context, the Business Process Execution Language for Web Services (bpel for short) has emerged as the de facto standard for implementing and composing Web services and, for this reason, it is supported by several major software vendors (Oracle Process Manager, IBM WebSphere, and Microsoft BizTalk).

The main issue concerning the publication of Web services is the definition of appropriate service descriptions that enable their identification, discovery and composition without revealing important details concerning their internal implementation. Service descriptions should retain abstract (behavioral) definitions separate from the binding to a concrete protocol. The current standard for service description is defined by the Web Service Description Language (wsdl) [START_REF] Christensen | Web Services Description Language ( wsdl) 1.1[END_REF], which specifies the format of the exchanged messages -the schema -, the locations where the interactions are going to occur -the interface -, the transfer mechanism to be used (i.e. soap-rpc, or others), and basic service abstractions (one-way/asynchronous and request-response/synchronous patterns of conversations). These abstractions are very simple and inadequate for expressing arbitrary, possibly cyclic protocols of exchanged messages between communicating parties. That is, the information provided by wsdl is insufficient for verifying the behavioral compliance between parties. It is also worth to notice that other technologies, such as uddi registries (Universal Description, Discovery and Integration [START_REF] Beringer | Using wscl in a uddi Registry 1.0[END_REF]), provide limited support because registry items only include pointers to the locations of the service abstractions, without constraining the way these abstractions are defined or related to the actual implementations (cf. the <tModel> element in the uddi specification). In this respect, uddi registries are almost useless for discovering services; an operation that is performed manually by service users and consumers. The publication of abstract service descriptions, which we call contracts in the following, and the related ability of service discovery call for the definition of a formal notion of contract equivalence and, more generally, of a formal theory for reasoning about Web services by means of their contracts. We identify three main goals of a theory of Web service contracts:

(G1) it should provide a formal language for describing Web services at a reasonable level of abstraction and for admitting static correctness verification of client/service protocol implementations; (G2) it should provide a semantic notion of contract equivalence embodying the principle of safe Web service replacement. Indeed, the lack of a formal characterization of contracts only permits excessively demanding notions of equivalence such as nominal or structural equality; (G3) it should provide tools for effectively and efficiently searching Web services in Web service repositories according to their contract.

The aim of this contribution is to provide a suitable theory of contracts for Web services. The main outcomes of our theory are summarized in Figure 1 and discussed below.

To pursue our investigation, in Section 2 we formalize an abstract language of bpel activities whose operators correspond to those found in bpel. The terms of this language, noted T , P 1 , and P 2 in Figure 1, capture the abstract communication behavior of bpel ignoring the syntactical details of schemas as well as those aspects that are oriented to the actual implementations, such as the definition of transmission protocols; all these aspects may be easily integrated on top of the formalism. We do not commit to a particular interpretation of the actions occurring in terms either: they can represent different typed channels on which interactions occur or different types of messages.

We equip abstract bpel activities with a semantics by resorting to a testing approach [START_REF] De Nicola | Testing equivalences for processes[END_REF]. In particular, we define client satisfaction, called compliance, as the ability of the client to successfully complete every interaction with the service; here "successfully" means that the client never gets stuck (this notion is purposefully asymmetric as client's satisfaction is our main concern). Compliance is noted in Figure 1. Then we derive a compliance preorder by comparing the sets of clients satisfied by bpel activities: two bpel activities are equivalent if they satisfy the same clients. In Section 4 we demonstrate that this preorder does coincide with a well-known semantics in concurrency theory, the must-testing semantics. The equivalence relation induced by compliance is noted in Figure 1.

The must-testing characterization of the compliance preorder leads us to define in Section 3 the notion of Web service contract, which allows us to solve goal (G1) above. In fact, these contracts, noted τ , σ 1 , and σ 2 in the above figure, are must-testing normal forms of activities that do not manifest internal moves and the parallel structures. That is, it is possible to describe abstract bpel activities without any loss of precision as far as the observable behavior of bpel activities is concerned.

In practice, the compliance preorder is a fine-grained semantics of bpel activities that forbids two important properties useful for service discovery. These properties are called width and depth extension. By width extension we mean the replacement of a service with another one that provides new functionalities (called methods, in the Web service terminology); by depth extension we mean the replacement of a service with another one that allows for longer communications beyond the terminal states of the original service. In Section 4, we define a variant of the compliance preorder, called subcontract preorder and noted in Figure 1, which supports these forms of extensions. Surprisingly, and notwithstanding the differences in the corresponding preorder relations, the equivalence induced by and do coincide. This means that, if a client is subcontract-compliant with a contract σ 1 then it will be subcontract-compliant with the corresponding abstract bpel activity P 1 , as well as with every activity P 2 that (width/depth-) extends P 1 . The definition of the subcontract preorder allows us to solve goal (G2).

We then analyze the problem of querying a repository of bpel activities. In Section 5, we show that it is possible to determine, given a client T exposing a certain behavior ρ, the smallest service contract (according to the subcontract preorder) that satisfies the client -the dual contract, noted D ρ in Figure 1. This contract, acting like a principal type in type systems, guarantees that a query to a Web service registry is answered with the largest possible set of compatible services in the registry's databases. This notion of duality allows us to solve goal (G3).

As a further validation step for our theory, we show that the subcontract relation is well behaved when applied to choreographies of Web services [START_REF] Kavantzas | Web Services Choreography Description Language 1.0[END_REF]. A choreography is an abstract specification of several endpoint services that run in parallel and communicate with each other by means of private names. In Section 6, we demonstrate that is robust enough so that, replacing an end-point service with another one retaining a larger contract, the compliance properties of the choreography are preserved.

Origin of the material. The basic ideas of this article have appeared in conference proceedings. In particular, the theory of contracts we use is introduced in [START_REF] Laneve | The must preorder revisited -an algebraic theory for web services contracts[END_REF] while the relation between (abstract) bpel activities and contracts has been explored in [START_REF] Laneve | An Algebraic Theory for Web Service Contracts[END_REF]. This article is a thoroughly revised and enhanced version of [START_REF] Laneve | The must preorder revisited -an algebraic theory for web services contracts[END_REF][START_REF] Laneve | An Algebraic Theory for Web Service Contracts[END_REF] that presents the whole framework in a uniform setting and includes the full proofs of all the results. A more detailed comparison with other related work is postponed to Section 7.

BPEL Abstract Activities

A Quick Look at BPEL

In bpel, business processes are described as the (sequential, alternative, parallel) composition of basic activities, in particular the sending/receiving messages. We introduce the basic notions of bpel looking at a stripped off version of the initial business process example in the language specification [START_REF] Alves | Web Services Business Process Execution Language Version 2.0[END_REF]. The xml document in Figure 2 describes the behavior of an e-commerce service that interacts with four other partners, one of them being the customer (identified by the name purchasing in the figure), the other ones being a service (identified by invoicing) that provides prices, a service (identified by shipping) that takes care of the shipment of goods, and a service (identified by scheduling) that schedules the manufacturing of goods. The business process is made of activities, which can be either atomic or composite. In this example atomic activities consist of the invocation of operations in other partners (lines 10-14, 22-27, 31-36), the acceptance of messages from other partners, either as incoming requests (line 3) or as responses to previous invocations (lines 15-19 and 28), and the sending of responses to clients (line 39). Atomic activities are composed together into so-called structured activities, such as sequential composition (see the sequence fragments) and parallel composition (see the flow fragment at lines . In a sequence fragment, all the child activities are executed in the order in which they appear, and each activity begins the execution only after the previous one has completed. In a flow fragment, all the child activities are executed in parallel, and the whole flow activity completes as soon as all the child activities have completed. It is possible to constrain the execution of parallel activities by means of links. In the example, there is a link ship-to-invoice declared at line 6 and used in lines 12 and 25, meaning that the invocation at lines 23-27 cannot take place before the one at lines 10-14 has completed. Similarly, the link ship-to-scheduling means that the invocation at lines 32-36 cannot take place before the receive operation at lines 15-19 has completed. In short, the presence of links limits the possible interleaving of the activities in a flow fragment.

bpel includes other conventional constructs not shown in the example, such as conditional and iterative execution of activities. For example, the bpel activity <if> <condition> bool-expr </condition> activity-True <else> activity-False </else>

::= 0 (empty) | a (receive) | a (invoke) | i∈I α i ; P i (pick) | P | A Q (flow & link) | P ;Q (sequence) | i∈I P i (if) | P * (while)
</if> evaluates bool-expr, which must be a Boolean condition, and executes either activity-True or activity-False depending on whether the condition turns out to be true or false. Similarly, the activity <while> <condition> bool-expr </condition> activity </while> specifies that activity should be repeatedly executed as long as the Boolean condition bool-expr is true.

A Formal Model of BPEL Abstract Activities

To pursue our formal investigation, we will now present an abstract language of activities whose operators correspond to those found in bpel.

We use a set N of names, ranged over by a, b, c, . . . , that represent communication channels or message types and a disjoint set N of co-names, ranged over by a, b, c, . . . ; the term action refers to names and conames without distinction; actions are ranged over by α, β, . . . . We use A, B, . . . to range over sets of names and we define an involution • such that a = a. We use ϕ, ψ, . . . to range over (N ∪ N) * and r, s, . . . to range over finite sets of actions. Let

r def = {α | α ∈ r}.
The syntax of bpel abstract activities is defined by the grammar in Table 1, where each construct has been named after the corresponding xml tag in bpel. Essentially we represent bpel abstract activities as terms of a simple process algebra similar to Milner's CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF] and Hoare's CSP [START_REF] Brookes | A theory of communicating sequential processes[END_REF]. Since we will focus on the interactions of bpel activities with the external environment rather than on the actual implementation of business processes, our process language overlooks details regarding internal, unobservable computations and focuses on the communication behavior of activities.

The activity 0 represents the completed process that performs no actions. The activity a represents the act of waiting for an incoming message. Here we take the point of view that a stands for a particular operation implemented by the process. The activity a represents the act of invoking the operation a provided by another partner. The activity i∈I α i ;P i represents the act of waiting for any of the α i operations to be performed, i belonging to a finite set I. Whichever operation α i is performed, it first disables the remaining ones and the continuation P i is executed. If α i = α j and i = j, then the choice whether executing P i or P j is implementation dependent. The process P | A Q, where A is a set of names, represents the parallel composition (flow) of P and Q and the creation of a private set A of link names that will be used by P and Q to synchronize; an example will be given shortly. The n-ary version A i∈1..n P i of this construct may also be considered: we stick to the binary one for simplicity. The process P ;Q represents the sequential composition of P followed by Q. Again we only provide a binary operator, where the bpel one is n-ary. The process i∈I P i represents an internal choice performed by the process, that results into one of the finite I exclusive continuations P i . Finally, P * represents the repetitive execution of process P so long as an internally verified condition is satisfied.

The pick activity i∈1..n α i ;P i and the if activity i∈1..n P i will also be written In the following we treat (empty), (receive), and (invoke) as special cases of (pick), while at the same time keeping the formal semantics just as easy. In particular, we write 0 for α∈∅ α ;P α and α as an abbreviation for α∈{α} α ;0 (tailing 0 are always omitted).

α 1 ; P 1 + • • • + α n ;P n
As we have anticipated, the language omits the details about the conditions that determine which branch of an if is taken or how many times an activity is iterated. For example, the if activity shown at the end of Section 2.1 will be abstracted into the process activity-True ⊕ activity-False, meaning that one of the two activities will be performed and the choice will be a consequence of some unspecified internal decision. A similar observation pertains to the <while> activity (see also Remark 2.2).

Example 2.1. The bpel activity in Figure 2 can be described by the term below, where for the sake of readability we give short names to the operations used in the activity as by

Note that we use names for specifying both actions and links. For example, we represent the source of the link ship-to-invoice as the action sti and the corresponding target as the action sti. Since sti guards the actions sSP and sI, these will not be executed until after rS, which guards sti, has been executed. Similarly for the ship-to-scheduling link. Note that names corresponding to links are restricted so that they are not visible from outside. Indeed, we will see that they do not appear in activity's behavioral description.

Remark 2.1. The bpel specification defines a number of static analysis requirements beyond the mere syntactic correctness of processes whose purpose is to "detect any undefined semantics or invalid semantics within a process definition" [START_REF] Alves | Web Services Business Process Execution Language Version 2.0[END_REF]. Several of these requirements regard the use of links. For example, it is required that no link must cross the boundary of a repeatable construct (while). It is also required that link ends must be used exactly once (hence 0 | {a} a is invalid because a is never used), and the dependency graph determined by links must be acyclic (hence a.b | {a,b} b.a is invalid because it contains cycles). These constraints may be implemented by restricting the arguments to the above abstract activities and then using static analysis techniques.

Operational Semantics of BPEL Abstract Activities

The operational semantics of bpel abstract activities is defined in Table 3. In the table we define two relations: P , read P has completed, and P µ -→ Q, where µ ranges over actions and the special name ε denoting internal computations, as the least ones satisfying the corresponding rules. The table does not report the symmetric rules for |.

According to Table 3, the process i∈I α i ; P i has as many α-labelled transitions as the number of actions in {α i | i ∈ I}. After a visible transition, only the selected continuation is allowed to execute. The process i∈I P i may internally choose to behave as one of the P i , with i ∈ I. The process P | A Q allows P and Q to internally evolve autonomously, or to emit/receive messages on names not in the set A, or to synchronize with each other on names in A. It completes when both P and Q have completed. The process P ;Q reduces according to the reductions of P first, and of Q when P has completed. Finally, the process P * may either complete in one step by reducing to 0, or it may execute P one more time followed by P * . The choice among the two possibilities is performed internally.

Predicate P 0 P Q P | A Q P Q P ;Q Transition relation P µ -→ Q (action) i∈I α i ; P i αi -→ P i (if) i∈I P i ε -→ P i (flow) P µ -→ P µ ∈ A ∪ A P | A Q µ -→ P | A Q (link) P α -→ P Q α -→ Q α ∈ A ∪ A P | A Q ε -→ P | A Q (seq) P µ -→ P P ;Q µ -→ P ; Q (seq-end) P Q µ -→ Q P ; Q µ -→ Q (while-
Remark 2.2. According to the operational semantics, P * may execute the activity P an arbitrary number of times. This is at odds with concrete bpel activities having P * as abstract counterpart. For example, the bpel activity <while> <condition> bool-expr </condition> activity </while> executes activity as long as the bool-expr condition is true. Representing such bpel activity with activity * means over-approximating it. This abstraction is crucial for the decidability of our theory.

We illustrate the semantics of bpel abstract activities through few examples: In the following we write A relevant property of our bpel abstract calculus is that the model of every activity P , that is the set of processes reachable from P by means of arbitrary reductions, is always finite. We introduce a number of auxiliary definitions that will be useful in the rest of the paper. By Lemma 2.1 these notions are trivially decidable. Definition 2.1. We introduce the following notation:

• We say that P diverges, notation P ↑, if there is an infinite sequence of ε-transitions P ε -→ ε -→ • • • starting from P . We say that P converges, notation P ↓, if it does not diverge.

• We let init(P ) def = {α | P α =⇒} be the set of initial visible actions performed by P .

• We say that P has ready set r, notation P ⇓ r, if

P ε =⇒ Q and r = init(Q). • Let P α =⇒. Then P (α) def = P ε =⇒ α -→Q Q.
We call P (α) the continuation of P after α. These definitions are almost standard, except for P (α) (that we already used in [START_REF] Laneve | The must preorder revisited -an algebraic theory for web services contracts[END_REF]). The abstract activity P (α) represents the residual behavior of P after an action α, from the point of view of the party that is interacting with P . Indeed, the party does not know which, of the possibly multiple, α-labelled branches P has taken. For example (a; b

+ a; c + b;d)(a) = b ⊕ c and (a; b + a ;c + b; d)(b) = d.

The Compliance Preorder

We proceed defining a notion of equivalence between abstract activities that is based on their observable behavior. To this aim, we introduce a special name e (not in N) for denoting the successful termination of an abstract activity ("e" stands for end). We let T range over client activities, that is activities that may contain such special name e. By compliance between a "client" activity T and a "service" activity P we mean that every interaction between T and P , where P stops communicating with T , is such that T has reached a successfully terminated state. Following De Nicola and Hennessy's approach to process semantics [START_REF] De Nicola | Testing equivalences for processes[END_REF], this compliance relation induces a preorder on services on the basis of the set of client activities that comply with a given service activity. Definition 2.2 (Compliance). The (client) activity T is compliant with the (service) activity P , written

T P , if P | N T ε =⇒ P | N T implies: 1. if P | N T ε -→, then {e} ⊆ init(T ), and 2. if P ↑, then {e} = init(T ).
The compliance preorder is the relation induced by compliance: P ∼ Q if and only if T P implies T Q for every T . We write for ∼ ∩ ∼ .

According to the notion of compliance, if the client-service conversation terminates, then the client is in a successful state (it will emit an e-name). -→ where the client waits for an interaction on a in vain. Similarly, the client must reach a successful state if the conversation does not terminate but the divergence is due to the service. In this case, however, every reachable state of the client must be such that the only possible action is e. The practical justification of such a notion of compliance derives from the fact that connection-oriented communication protocols (like those used for interaction with Web services) typically provide for an explicit end-of-connection signal. Consider for example the client behavior e + a ;e. Intuitively this client tries to send a request on the name a, but it can also succeed if the service rejects the request. So e + a ;e 0 because the client can detect the fact that the service is not ready to interact on a. The same client interacting with a diverging service would have no way to distinguish a service that is taking a long time to accept the request from a service that is perpetually performing internal computations, hence e + a; e Ψ. As a matter of facts, the definition of compliance makes Ψ the "smallest service" -the one a client can make the least number of assumptions on (this property will be fundamental in the definition of principal dual contract in Section 5). That is Ψ ∼ P , for every P . As another example, we notice that a; b + a ;c ∼ a ;(b ⊕ c) since, after interacting on a, a client of the smaller service is not aware of which state the service is in (it can be either b or c). As by Definition 2.2, it is difficult to formally show the compliance preorder between two activities because of the universal quantification over all (client) activities T . For this reason, in Section 4, we will provide an alternative characterization of ∼ that allows us to prove the compliance preorder without any universal quantification.

Contracts

In this section we discuss how to associate a behavioral description, called contract, to a bpel abstract activity. There is always a tradeoff between details and abstraction when defining contracts. In general, two criteria should be taken in consideration:

(1) contracts, being public, should conceal the internal structure of activities or local links, i.e. the actual implementation of services; (2) it should be possible to reason about the "relevant properties" of bpel activities by means of the respective contracts.

Since in our case the "relevant property" mentioned in ( 2) is compliance, we will require contracts to be compliant (equivalent) with the corresponding bpel activities. This limits our range of abstract descriptions to models of the compliance preorder and the following behavioral descriptions are one of such models. We consider a set of contract names, ranged over C, C , C 1 , . . . . A contract is a tuple

(C 1 = σ 1 , . . . , C n = σ n , σ)
where C i = σ i are contract name definitions, σ is the main term, and we assume that there is no chain of definitions of the form

C n1 = C n2 , C n2 = C n3 , . . . , C n k = C n1 .
The syntax of the σ i 's and of σ is given by the grammar below:

σ ::= C | α ; σ | σ + σ | σ ⊕ σ
where C ∈ {C 1 , . . . , C n }. The contract α ;σ represents sequential composition in the restricted form of prefixing. The operators + and ⊕, referred to as external and internal choice, correspond to pick and if of bpel activities, respectively. These operations are assumed to be associative and commutative; therefore we will write [OutOfStock]

σ 1 + • • • + σ n and σ 1 ⊕ • • • ⊕ σ n without
[InvalidLogin]

[InvalidPayment]

[Accepted]

[OutOfStock]

[InvalidPayment] Fig. 3. Contract of a simple e-commerce service as a wscl diagram.

The operational semantics of contracts is defined by the rules below:

α ;σ α -→ σ σ ⊕ ρ ε -→ σ σ ε -→ σ σ + ρ ε -→ σ + ρ σ α -→ σ σ + ρ α -→ σ C = σ σ µ -→ σ C µ -→ σ
plus the symmetric of rules + and ⊕. Note that + evaluates the branches as long as they can perform invisible actions. This rule is absent in bpel abstract activities because, there, the branches are always guarded by an action.

In the following we will use these definitions:

• 0 def = C 0 , where C 0 = C 0 + C 0 represents a terminated activity; • Ω def = C Ω , where C Ω = C Ω ⊕ C Ω represents divergence, that is a non-terminating activity.
In particular, there are no µ and σ such that 0 µ -→ σ and Ω ε -→ Ω is the only transition of Ω. Although the contract language is apparently simpler than bpel abstract activities, it is not a sublanguage of the latter. In fact, Ω cannot be written as a term in the syntax of Section 2. Nevertheless, in the following we will demonstrate that contracts provide alternative descriptions (with respect to the preorder ∼ ) to bpel abstract activities.

Example 3.1. The Web service conversation language wscl [START_REF] Banerji | Web Services Conversation Language ( wscl) 1.0[END_REF] describes conversations between two parties by means of an activity diagram (Figure 3). The diagram is made of interactions connected with each other by transitions. An interaction is a basic one-way or two-way communication between the client and the server. Two-way communications are just a shorthand for two sequential one-way interactions. Each interaction has a name and a list of document types that can be exchanged during its execution. A transition connects a source interaction with a destination interaction. A transition may be labeled by a document type if it is active only when a message of that specific document type was exchanged during the previous interaction.

The diagram in Figure 3 describes the conversation of a service requiring clients to login before they can issue a query. After the query, the service returns a catalog. From this point on, the client can decide whether to purchase an item from the catalog or to logout and leave. In case of purchase, the service may either report that the purchase is successful, or that the item is out-of-stock, or that client's payment is refused. By interpreting names as message types, this e-commerce service can be described by the tuple:

( C 1 = Login ;(InvalidLogin ;C 1 ⊕ ValidLogin ;C 2 ) , C 2 = Query ;Catalog ; (C 2 + C 3 + C 4 ) , C 3 = Purchase ;( Accepted ⊕ InvalidPayment ;(C 3 + C 4 ) ⊕ OutOfStock ;(C 2 + C 4 ) ) , C 4 = Logout , C 1 )
There is a strict correspondence between unlabeled (respectively, labeled) transitions in Figure 3 and external (respectively, internal) choices in the contract. Recursion is used for modeling the cycles in the figure, namely the behaviors that can be iterated. We can relate bpel abstract activities and contracts by means of the corresponding transition systems. To this aim, let X and Y range over bpel abstract activities and contracts. Then, X and Y interact according to the rules

X µ -→ X µ / ∈ A ∪ A X | A Y µ -→ X | A Y Y µ -→ Y µ / ∈ A ∪ A X | A Y µ -→ X | A Y X α -→ X Y α -→ Y α ∈ A ∪ A X | A Y ε -→ X | A Y
It is possible to extend the definition of compliance to contracts and, by Definition 2.2, obtain a relation that allows us to compare activities and contracts without distinction. To be precise, the relation X ∼ Y is smaller (in principle) than the relation ∼ given in Definition 2.2 because, as we have said, the contract language is not a sublanguage of that of activities and, therefore, the set of tests that can be used for comparing X and Y is larger. Nonetheless, in Section 4, we demonstrate that ∼ of Definition 2.2 coincides with the relation X ∼ Y. This is a key point of our development, which will allow us to safely use the same symbol ∼ for both languages and to define, for every activity P , a contract σ P such that P σ P . In particular, we let C P be the contract name defined by

C P =    Ω if P ↑ P ⇓r α∈r α ; C P (α) otherwise
Intuitively, when P diverges, the contract C P associated with P is the canonical diverging contract Ω. When P converges, then C P has as many top-level states as the ready sets of P , which are in correspondence with all the residuals to which P may reduce by means of invisible moves. For each ready set r of P , the contract of P exposes all and only the visible actions α in r and continues as C P (α) . We illustrate the computation of C P by means of an example.

C P = Login ;C (InvalidLogin ;Login) * ; ValidLogin ; Q C (InvalidLogin ;Login) * ; ValidLogin ;Q = InvalidLogin ;C P ⊕ ValidLogin ;C Q C Q = • • •
Observe that the contract C 1 in Example 3.1, which corresponds to the same activity P , is syntactically different from the one we obtain above. Using the techniques we develop in the next section, it is possible to demonstrate that the two contracts are equivalent.

A relevant property of C P is an immediate consequence of Lemma 2.1.

Lemma 3.1. For every P , the set cnames(C P ) is finite.

The construction of the contract C P with respect to a bpel abstract activity P is both correct and complete with respect to compliance:

Theorem 3.1. P C P .
This result allows us to define flow & link-free ∼ -normal forms of abstract bpel activities. Such normal forms are as intelligible as wscl conversation diagrams, independently defined at Hewlett-Packard with the exact purpose of specifying the abstract interfaces supported by a concrete services.

Compliance, Must-testing and Subcontracts

Properties of Compliance

As by Definition 2.2, it is difficult to understand the general properties of the compliance preorder because of the universal quantification over all (client) activities T . For this reason, it is convenient to provide an alternative characterization of ∼ which turns out to be the one below. Following the same convention of Section 3, we will let X and Y range over bpel abstract activities and contracts. We write for the largest coinductive compliance relation.

According to this definition, a term X such that X↑ is the smallest one. When X↓, condition 1 requires the larger term Y to converge as well, since clients might rely on the convergence of X to complete successfully. Condition 2 states that each ready set r of Y (that is, each state reachable from Y by means of invisible moves only) is matched by a corresponding ready set s of X such that s ⊆ r. This is to say that Y exhibits a more deterministic behavior than X and that Y exposes at least the same capabilities as X. Condition 3 demands that Y should provide no more actions than those provided by X and that the corresponding continuations for any such action α be related by coinductive compliance. The rationale for using the continuations X(α) and Y(α) rather than simply any pair of derivatives of X and Y (as would be in a standard simulation relation) is motivated by the fact that clients are unaware of the internal choices performed by services. So, for example, a; b + a; c a; (b ⊕ c) because, after interacting on a, a client of the service on the left hand side of is not aware of which state the service is in (it can be either b or c). By considering the continuations after a, we end up verifying b ⊕ c R b ⊕ c, which trivially holds for every coinductive compliance relation.

By now we have defined a range of compliance relations: a semantic one (Definition 2.2) between abstract BPEL activities and a coinductive one . Definition 2.2 can also be adapted according to the set of tests that we take into account. In particular, let ∼C be the compliance relation when tests T are contracts and let ∼A+C be the compliance relation of Definition 2.2 when tests T can be either abstract activities or contracts. Clearly X ∼A+C Y implies both X ∼ Y and X ∼C Y, while in principle the converse may be false. The following theorem guarantees the coincidence of all the compliance relations defined thus far and shows that is a coinductive characterization of them.

Theorem 4.1. For every X and Y, the following statements are equivalent:

1. X Y; 2. X ∼ Y; 3. X ∼C Y; 4. X ∼A+C Y.
By relating a testing semantics and a coinductive semantics, Theorem 4.1 bridges the gap between the two techniques and allows one to choose the corresponding arguments interchangeably. Similar results have been provided for the lazy lambda calculus by Abramsky [START_REF] Abramsky | The lazy lambda calculus[END_REF] and, more recently, for the lambda calculus with local store by Pitts and Stark [START_REF] Pitts | Observable properties of higher order functions that dynamically create local names, or what's new[END_REF]. Thanks to Theorem 4.1, in the rest of the paper we will just use the symbol ∼ to denote both ∼A+C and ∼C .

An application of Theorem 4.1 is to relate two apparently different testing semantics for abstract activities (and contracts): the compliance preorder and the must-testing preorder [START_REF] Hennessy | Algebraic Theory of Processes[END_REF]. To this aim, we recall the definition of the must preorder. In accordance with Definition 2.2, we let T to range over activities/contracts that may contain the special name e. Definition 4.2 (Must preorder [START_REF] De Nicola | CCS without τ 's[END_REF]). A sequence of transitions

X 0 | N T 0 ε -→ X 1 | N T 1 ε -→ • • • is a maximal computation if either it is infinite or the last term X n | N T n is such that X n | N T n -→. Let X must T if, for every maximal computation X | N T = X 0 | N T 0 ε -→ X 1 | N T 1 ε -→ • • • , there exists n ≥ 0 such that T n e -→.
We write X must Y if and only if, for every T, X must T implies Y must T.

Before showing the precise relationship between ∼ and must , let us comment on the differences between X T and X must T. The must relation is such that σ must e + ρ holds for every σ, so that the observers of the form e + ρ are useless for discriminating between different (service) behaviors in must . However this is not the case for . For example e + a a whilst a must e + a. In our setting it makes no sense to declare that e + a is compliant with a with the justification that, at some point in a computation starting from e + a | a, the client can emit e. When a client and a service interact, actions cannot be undone. On the other hand we have e ⊕ e Ω and Ω must e ⊕ e. That is a (client) behavior compliant with a divergent (service) behavior is such that it is compliant with every (service) behavior. Hence e ⊕ e is useless for discriminating between different services. Historically, Ω must e ⊕ e has been motivated by the fact that the divergent process may prevent the observer from performing the one internal reduction that leads to success. In a distributed setting this motivation is no longer sustainable, since client and service will usually run independently on different processors. Finally, consider a divergent (client) behavior ρ. In the must relation such observer never succeeds unless ρ e -→. In the relation such observer is compliant so long as all of its finite computations lead to a successful state. So, for example, the client behaviors C = a ;e ⊕ C and a; e have the same discriminating power as far as ∼ is concerned.

Notwithstanding the above different testing capabilities, must and ∼ do coincide. As by Theorem 4.1, this is proved by demonstrating the equality of must and . Incidentally, Theorem 4.2, by relating must and ∼ , provides a coinductive characterization of must , which is, to the best of our knowledge, original in [START_REF] Laneve | The must preorder revisited -an algebraic theory for web services contracts[END_REF].

The Subcontract Relation

Theorems 3.1 and 4.2 show that ∼ and must-testing are just the right relations to reason about (abstract) BPEL activities and their own contracts, since they are defined taking Web service clients as tests for discriminating between behaviors. Yet, there are contexts in which these relations are too strong, in particular when querying a repository of Web service contracts. In these cases, it is reasonable to work with a weaker notion of "service compatibility" that enables two useful properties called width and depth extension.

To illustrate, consider a service whose contract is a ;c, namely a service that receives a request a to which it answers with a response c. It is reasonable to expect that, if the service is extended with a new functionality, let us say a ;c + b;d, the clients of the original service will still comply with the extended one. Regrettably, this is not the case; for example, we have a; c;e + b a; c and a ;c; e + b a ;c + b;c, that is a; c; e + b succeeds with the original service, but fails with the extended one, witnessing that a; c ∼ a ;c + b; c. This is an instance of width extension failure, whereby it is not possible to extend the behavior of a service with new operations offered by means of external choices. Similarly, extending the service a; c to a; c;b; d is not allowed by ∼ because a; c; (e + b) a; c and a; c;(e + b) a ;c; b; d. This is an instance of depth extension failure, whereby it is not possible to prolong the behavior of a service beyond its terminal states.

Both width and depth extension failures are a consequence of the fact that, among the clients of the original service (contract) a ;c, we respectively admit a; c;e + b and a; c;(e + b) which are specifically (and possibly maliciously) crafted to sense an operation b not provided by the original service and to fail as soon as this operation is provided by the extended one. The existence of these clients is what makes compliance conservative, because ∼ quantifies over all possible clients, including malicious ones. To define a coarser relation between contracts, one that allows both width and depth extensions, we restrict the set of clients (hence, of tests) that are compliant to (the contract of) an activity to those that never perform unavailable operations. To do so, following [START_REF] Laneve | The must preorder revisited -an algebraic theory for web services contracts[END_REF], we switch to more informative contracts than those described in Section 3. In particular, we consider pairs i : σ, called extended contracts, where σ is a term as in Section 3 and i ⊇ actions(σ) is a finite set of actions that defines the interface of the service whose behavior is described by σ. Then, we define a subcontract relation along the lines of Definition 2.2, except that we consider as tests only those clients that respect the interface of a contract, namely that do not request operations other than those in the interface of the contract.

Definition 4.3 (Subcontract relation).

Let i : σ j : τ if i ⊆ j and, for every k : ρ such that k \ {e} ⊆ i and ρ σ implies ρ τ . Let ≈ be ∩ .

Notice that i : σ j : τ only if i ⊆ j. This apparently natural prerequisite has substantial consequences on the properties of because it ultimately enables width and depth extensions, which are not possible in the ∼ preorder. For instance, we have {a} : a {a, b} : a + b whilst a ∼ a + b (width extension). Similarly we have {a} : a {a, b} : a ;b whilst a ∼ a ;b (depth extension).

To highlight the relevant properties of and conforming to the same pattern used for ∼ , we provide an alternative characterization of , which is also convenient in proofs. The characterization is similar to the one of Definition 4.1. Definition 4.4. A coinductive subcontract is a relation R such that if i : σ R j : τ , then i ⊆ j and whenever σ↓ we have:

1. τ ↓, and 2. τ ⇓ r implies σ ⇓ s and s ⊆ r, and 3. α ∈ i and τ α =⇒ imply σ α =⇒ and i : σ(α) R j : τ (α). Definition 4.4 is structurally very similar to Definition 4.1, with two relevant differences: the first one is the condition i ⊆ j, which follows directly from Definition 4.3; the second and fundamental one is that, in condition (3), only the actions α that were already present in the smaller contract are taken into account when considering the continuations. This way, any behavior provided by the larger contract that follows an action α which is not in the interface of the smaller contract need is ignored. Definition 4.4 completely characterizes the subcontract relation:

Theorem 4.3.
is the largest coinductive subcontract relation.

The next proposition summarizes the most relevant properties of in a formal way. In particular, it emphasizes the width and depth extensions allowed by but forbidden in ∼ and in the must-testing preorder. The proof of these properties is easy using the alternative characterization of in Definition 4.4).

Proposition 4.1. The following properties hold:

1. If i : σ j : τ and i : σ j : τ , then i : σ j : τ ⊕ τ ; 2. if i : 0 j : τ , then i : σ j : σ + τ (width extension); 3. if i : 0 j : τ , then i : σ j : σ{ τ / 0 }, where σ{ τ / 0 } is the replacement of every occurrence of the contract name 0 with τ (depth extension).

Item 1 states that the clients that are compliant with both contracts j : τ and j : τ are also compliant with services that internally decide to behave according to either τ or τ . Item 2 gives sufficient conditions for width extensions of Web services: a Web service may be upgraded to offer additional functionalities without affecting the set of clients it satisfies, so long as the names of such new functionalities were not present in the original service. Here the premise i : 0 j : τ formalizes the concept of "new functionality": any action α such that τ α =⇒ must be in j \ i and in particular it cannot be an action of σ. Additionally, the same premise implies that τ ↓, because we have 0↓ (see Definition 4.4). Item 3 is similar to item 2, but concerns depth extensions, that is the ability to extend the conversation offered by a service, provided that the additional conversation begins with new functionalities not present in the original service. In fact, item 2 can be seen as a special case of item 3, if we consider the contract i : σ + 0 instead of simply i : σ.

The precise relationship between and ∼ is expressed by the following statement. Proposition 4.2. i : σ ≈ j : τ if and only if σ τ and i = j.

Duality

We now analyze the problem of querying a repository of bpel activities, where every activity P is modeled by the extended contract i P : C P such that i P = actions(C P ) and C P is defined in Section 3. The basic problem for querying such a repository is that, given a client's extended contract k : ρ, one wishes to find all the pairs i : σ such that k \ {e} ⊆ i and ρ σ.

We attack this problem in two steps: first of all, we compute one particular extended contract k\{e} : D k ρ , called dual of k : ρ, such that ρ D k ρ ; second, we collect all the services in the registry whose extended contract is larger (according to ) than this one. To be sure that no suitable service is missing in the answer to the query, the dual of a client k : ρ should be a pair k \ {e} : D k ρ that it is the smallest one (according to ) that satisfies the client k : ρ. We call such pair the principal dual extended contract of k : ρ.

In defining the principal dual extended contract, it is convenient to restrict the definition to those client's behaviors ρ that never lead to 0 without emitting e. For example, the behavior a ;e + b describes a client that succeeds if the service proposes a, but that fails if the service proposes b. As far as querying is concerned, such behavior is completely equivalent to a; e. As another example, the degenerate client behavior 0 is such that no service will ever satisfy it. In general, if a client is unable to handle a particular action, like b in the first example, it should simply omit that action from its behavior. We say that a (client) extended contract Observe that Lemma 2.1 also applies to contracts. Therefore it is possible to extend the notions in Definition 2.1, by replacing activities with contracts.

k : ρ is canonical if, whenever ρ ϕ =⇒ ρ is
D k ρ def =        Ω if init(ρ) = {e} ρ ⇓ r r\{e} = ∅ 0 ⊕ if e ∈ r α∈r\{e} α ; D k ρ(α) + E k\init(ρ) otherwise E s def = 0 ⊕ α∈s α ; Ω if s = ∅
Few comments about D k ρ , when init(ρ) = {e}, follow. In this case, the behavior ρ may autonomously transit to different states, each one offering a particular ready set. Thus the dual behavior leaves the choice to the client: this is the reason for the external choice in the second line. Once the state has been chosen, the client offers to the service a spectrum of possible actions: this is the reason for the internal choice underneath the sum .

The contract E k\init(ρ) covers all the cases of actions that are allowed by the interface and that are not offered by the client. The point is that the dual operator must compute the principal (read, the smallest) service contract that satisfies the client, and the smallest convergent behavior with respect to a nonempty (finite) interface s is 0 ⊕ α∈s α ; Ω. The 0 summand accounts for the possibility that none of the actions in k \ init(ρ) is present. The external choice "+" distributes the proper dual contract over the internal choice of all the actions in k \ init(ρ). For example, D , where

D k C 1 = Login ; D k C 2 + E k\{Login} D k C 2 = (InvalidLogin ;D k C 1 ⊕ ValidLogin ;D k C 3 ) + E k\{InvalidLogin,ValidLogin} D k C 3 = Query ; D k C 4 + E k\{Query} D k C 4 = Catalog ;D k C 5 + E k\{Catalog} D k C 5 = Logout ;Ω + E k\{Logout} Let k = k ∪ {Purchase, Accepted, InvalidPayment, OutOfStock}. We invite the reader to verify that k \ {e} : D k C 1 k \ {e} : C 1 , where C 1 has been defined in Example 3.1.
A basic property of the dual contract of k : ρ is that it defines the behavior of the least service compliant with k : ρ. This property, known in type theory as principal type property, guarantees that queries to service registries are answered with the largest possible set of compliant services. Theorem 5.1. Let k : ρ be a canonical extended contract. Then:

1. ρ D k ρ ; 2. if k \ {e} ⊆ s and ρ σ, then k \ {e} : D k ρ s : σ.
A final remark is about the computational complexity of the discovery algorithm. Deciding is EXPTIMEcomplete in the size of the contracts [START_REF] Aceto | The algoritmics of bisimilarity[END_REF], and this cost should, in principle, be multiplied by the number of services in the repository. However, since is (obviously) transitive (see Definition 4.3), it is reasonable to assume that Web service are ordered according to as soon as they are entered into the registry. Therefore, at runtime the relation must be decided only for the -minimal services, the remaining ones being determined by the (pre-computed) transitive closure.

Choreographies

A choreography is meant to describe the parallel composition of n services (called participants) that communicate with each other by means of private names and with the external world by means of public names. Standard languages for describing choreographies, such as the Web Service Choreography Description Language (ws-cdl [START_REF] Kavantzas | Web Services Choreography Description Language 1.0[END_REF]), allow an architect of a distributed system to focus on how the various inter-participant interactions happen by giving a global description (choreography) of the system, rather than describing the behavior of each single interacting peer (end-point behavior). In particular, this global description determines where and when a communication has to happen. That is, the architect decides that e.g. there will be a message from a peer A to a peer B and overlooks how this communication will be implemented.

In this section, having contracts at hand, we identify a choreography with the composition of its end-point projections, which are represented as extended contracts. This approach is standard in the literature, see for example [START_REF] Carbone | Structured communication-centered programming for web services[END_REF] and [START_REF] Bravetti | Towards a unifying theory for choreography conformance and contract compliance[END_REF]. Formally, a choreography is an ordered version of the n-ary flow and link term in Section 2:

Γ ::= A (i 1 : σ 1 , . . . , i n : σ n )
where A is a subset of names representing the private names of the choreography. We write Γ[i → j : ρ] for the choreography that is the same as Γ except that (the extended contract of) the i-th participant has been replaced by j : ρ.

The transition relation of choreographies is defined using that of behaviors by the following rules, where

Γ = A (i 1 : σ 1 , . . . , i n : σ n ): σ µ -→ σ µ / ∈ A ∪ A Γ[i → i : σ] µ -→ Γ[i → i : σ ] i = j σ α -→ σ τ α -→ τ α ∈ A ∪ A Γ[i → i : σ][j → j : τ ] ε -→ Γ[i → i : σ ][j → j : τ ]
That is, a choreography Γ = A (i 1 : σ 1 , . . . , i n : σ n ) is akin to a (compound) service whose interface is

actions(Γ) def = 1≤i≤n i i \ (A ∪ A)
and whose behavior is the combination of the behaviors of the end-point projections running in parallel.

Having provided choreographies with a transition relation, the notions of convergence, divergence, and ready set can be immediately extended to choreographies from Definition 2.1. Similarly, the notion of compliance may be extended in order to relate the behavior of a client with (the behavior of) a choreography, which we denote by ρ Γ. More precisely, we say that an extended (client) contract k : ρ is compliant with the choreography Γ if k \ {e} ⊆ actions(Γ) and ρ Γ, as in Definition 2.2.

In the remaining part of the section we show that the subcontract relation (Definition 4.3) suitably addresses the problem of contract refinement, namely it allows one to replace a given choreography Γ with a refined one Γ , where some or all the participants behave according to refined contracts, still preserving the correctness of the overall system. By correctness we mean that every client that was compliant with the original choreography is still compliant with the refined one. Technically, this shows that under mild conditions the relation is a pre-congruence with respect to parallel composition of services, and therefore can be efficiently used for modular refinement of complex systems.

Definition 6.1 (Choreography refinement). Let Γ =

A (i 1 : σ 1 , . . . , i n : σ n ) and Γ = A (j 1 : τ 1 , . . . , j n : τ n ) be choreographies. We say that Γ is a refinement of Γ if:

1. i i : σ i j i : τ i for every 1 ≤ i ≤ n; 2. (j i \ i i ) ∩ i j = ∅ for every 1 ≤ i, j ≤ n.
Refinement defines a "safe" replacement of activities in a choreography with refined ones (such as their implementations). The replacing activities may have more capabilities than those offered by the replaced ones (condition (1)), although the set A of private names must be the same in both the original and the refined choreography. This is to make sure that the original choreography specification is respected in the refinement. Additionally, there must be no interferences between the additional capabilities of the refined choreography with respect to those in the original choreography (condition (2)). In particular, every action that is introduced in the refinement of a peer must be disjoint from any other action of the original choreography. To illustrate the relevance of condition (2), consider the choreographies

Γ 1 def = ∅ ({a} : a, {b, c} : b;c) and Γ 2 def = ∅ ({a, b} : a + b, {b, c} : b; c)
and observe that each extended contract in Γ 1 is a subcontract of the corresponding one in Γ 2 , that is Γ 1 and Γ 2 satisfy condition (1) of Definition 6.1. Nonetheless, extending the first participant in Γ 1 to {a, b} : a + b in Γ 2 introduces an interference on b, which is an operation provided also by the second participant. For instance, the client behavior b; c; e is compliant with Γ 1 but not with Γ 2 . Condition (2) prevents Γ 2 from being a refinement of Γ 1 by forbidding the introduction of these interferences. In practice, this condition is not restrictive since operation names usually include the name of the participant which provides them. We now prove a soundness result for the notion of refinement. The result does not rely on any particular property (e.g. deadlock freedom) of the choreography itself. We merely show that, from the point of view of a client interacting with a choreography as a whole, the refinement of the choreography does not jeopardize the completion of the client. Theorem 6.1. Let k : ρ be compliant with Γ 1 and Γ 2 be a refinement of Γ 1 . Then k : ρ is also compliant with Γ 2 .

Related Work

Our contracts are normal forms of τ -less ccs processes, a calculus developed by De Nicola and Hennessy in a number of contributions [START_REF] De Nicola | CCS without τ 's[END_REF][START_REF] Hennessy | Algebraic Theory of Processes[END_REF][START_REF] Milner | A Calculus of Communicating Systems[END_REF]. The use of formal models to describe communication protocols is not new (see for instance the exchange patterns in ssdl [START_REF] Parastatidis | MEP SSDL Protocol Framework[END_REF], which are based on csp and the π-calculus), nor is it the use or ccs processes as behavioral types (see [START_REF] Nielson | Higher-order concurrent programs with finite communication topology (extended abstract)[END_REF] and [START_REF] Chaki | Types as models: model checking message-passing programs[END_REF]).

The theory of extended contracts and the subcontract relation has been introduced in [START_REF] Laneve | The must preorder revisited -an algebraic theory for web services contracts[END_REF][START_REF] Laneve | An Algebraic Theory for Web Service Contracts[END_REF]. There are several works studying theories of contracts for Web services. The ones more closely related to ours are by Carpineti et al. [START_REF] Carpineti | A formal account of contracts for Web Services[END_REF], by Castagna et al. [START_REF] Castagna | A Theory of Contracts for Web Services[END_REF] and by Padovani [START_REF] Padovani | Contract-Directed Synthesis of Simple Orchestrators[END_REF][START_REF] Padovani | Contract-Based Discovery and Adaptation of Web Services[END_REF][START_REF] Padovani | Contract-Based Discovery of Web Services Modulo Simple Orchestrators[END_REF]. In [START_REF] Carpineti | A formal account of contracts for Web Services[END_REF] the subcontract relation (over finite contracts) enjoys the width extension property illustrated in Section 4 but it lacks transitivity. Transitivity, while not being strictly necessary as far as querying and searching are concerned, allows databases of Web services contracts to be organized in accordance with the subcontract relation, so as to reduce the run time spent for executing queries. The transitivity problem has been also addressed in [START_REF] Castagna | A Theory of Contracts for Web Services[END_REF]. The authors of [START_REF] Castagna | A Theory of Contracts for Web Services[END_REF] make the assumption that client and service can be mediated by a filter, which prevents potentially dangerous interactions by dynamically changing the interface of the service as it is seen by the client. Even more expressive filters, akin to actual orchestrators, have been investigated in [START_REF] Padovani | Contract-Directed Synthesis of Simple Orchestrators[END_REF][START_REF] Padovani | Contract-Based Discovery and Adaptation of Web Services[END_REF][START_REF] Padovani | Contract-Based Discovery of Web Services Modulo Simple Orchestrators[END_REF]. In these cases the subcontract relation can be extended even further, by allowing (partial) permutation of actions whenever these do not disrupt the flow of messages between client and service. The present work can be seen as an optimization of the aforementioned works using filters/orchestrators in which the filter/orchestrator is represented as a static interface and therefore implies no runtime involvement of an active entity. At the same time, in the present work we also consider divergence, which is not addressed in [START_REF] Castagna | A Theory of Contracts for Web Services[END_REF][START_REF] Padovani | Contract-Directed Synthesis of Simple Orchestrators[END_REF][START_REF] Padovani | Contract-Based Discovery and Adaptation of Web Services[END_REF][START_REF] Padovani | Contract-Based Discovery of Web Services Modulo Simple Orchestrators[END_REF].

There are similarities between contracts and session types. While the former ones provide abstract descriptions of whole process behaviors, session types describe the behavior of a process with respect to a single communication channel. From a syntactical point of view, both session types and contracts are terms of simple process algebras made of prefixed actions and internal/external choices. The similarities carry on at the semantic level, since subtyping relations for session types are known to support width extensions [START_REF] Gay | Subtyping for session types in the π-calculus[END_REF]. With respect to [START_REF] Gay | Subtyping for session types in the π-calculus[END_REF] (and other systems based on session types) our contract language is simpler and can express more general forms of interaction. While the language defined in [START_REF] Gay | Subtyping for session types in the π-calculus[END_REF] supports first-class sessions and name passing, it is purposefully tailored so that the transitivity problems mentioned above are directly avoided at the language level. This restricts the subtyping relation in such a way that internal and external choices can never be related (hence, {a, b} : a ⊕ b {a, b} : a + b does not hold). A thorough analysis of the relationship between contracts and session types and between subcontract and subtyping relations have been investigated in [START_REF] Bernardi | Behavioural Equivalences for Web Services[END_REF][START_REF] Bernardi | Modelling session types using contracts[END_REF][START_REF] Laneve | The pairing of contracts and session types[END_REF].

The semantic characterization of the compliance preorder in Definition 2.2, which we have inherited from the testing framework [START_REF] De Nicola | Testing equivalences for processes[END_REF], allows one to introduce refinement relations that preserve, by definition, some desired property (in our case, client compliance). This style has been adopted in several subsequent works, in particular those dealing with liveness-preserving relations which are otherwise difficult to characterize. The interested reader may refer to [START_REF] Bugliesi | Compliance preorders for web services[END_REF] for liveness-preserving subcontract relations and to [START_REF] Padovani | Fair Subtyping for Multi-Party Session Types[END_REF][START_REF] Padovani | Fair Subtyping for Open Session Types[END_REF] for livenesspreserving subtyping relations for session types.

Behavioral descriptions of processes have been recently used for defining choreographies. In [START_REF] Honda | Multiparty asynchronous session types[END_REF], Carbone et al. define a model of ws-cdl and relate this model to session types. This model has been extended to cover exceptions in [START_REF] Carbone | Session-based choreography with exceptions[END_REF]. Contracts for end-point projections of choreographies, their semantics, and contract refinements have been studied by Bravetti et al. in a number of contributions [START_REF] Bravetti | Contract-driven implementation of choreographies[END_REF][START_REF] Bravetti | Contract-based discovery and composition of web services[END_REF][START_REF] Bravetti | A theory of contracts for strong service compliance[END_REF]. In particular they refine compliance in order to guarantee deadlock and livelock freedom of end-point composition and endpoint refinement (while we only guarantee client's successful completion). Differently from the present paper, in order to characterize the largest possible set of compatible peers a maximal peer refinement relation is defined instead of using the notion of dual contract. Such maximal relation exists only under some precise conditions, like in the case of asynchronously communicating services [START_REF] Bravetti | A foundational theory of contracts for multi-party service composition[END_REF] or for systems in which a receiver is required be ready to receive a message as soon as the emitter is ready to send it [START_REF] Bravetti | A theory of contracts for strong service compliance[END_REF]. In cases in which the maximal relation exists, it has been characterized by resorting to the should-test preorder.

Regarding schemas, which are currently part of bpel contracts, it is worth mentioning that they have been the subject of formal investigation by several research projects [START_REF] Benzaken | CDuce: an XML-centric general-purpose language[END_REF][START_REF] Carpineti | PiDuce -A Project for Experimenting Web Services Technologies[END_REF][START_REF] Hosoya | XDuce: A statically typed XML processing language[END_REF]. This work aims at pursuing a similar objective, but moving from the description of data to the description of behaviors.

Conclusions

In this contribution we have studied a formal theory of Web service abstract (behavioral) definitions as normal forms of a natural semantics for bpel activities. Our abstract definitions may be effectively used in any query-based system for service discovery because they support a notion of principal dual contract. This operation is currently done in an ad hoc fashion using search engines or similar technologies.

It should be noted that our framework rests on a correspondence between abstract activities as defined in Section 2 and bpel activities, noted "bpel Client", "bpel Service 1", and "bpel Service 2" in Figure 1, which cannot be completely formalized for the simple reason that bpel is not equipped with a formal semantics. In addition, bpel activities define details about internal computations that are omitted in the corresponding abstractions. In fact, models of bpel services are infinite state, while abstract bpel activities have finite models. However, our abstract bpel activities allow us to overapproximate bpel activities as far as the observable communication behavior is concerned by increasing non-determinism (for example, by representing a deterministic conditional construct as a non-deterministic choice P ⊕ Q). Roughly speaking, this means for instance that P 1 "bpel Service 1" in Figure 1 and we give some evidence of this fact in Section 2. A side-effect of this added non-determinism is that there may be bpel clients that successfully complete their interaction with a bpel service, while the compliance cannot be assessed between the corresponding abstract bpel activities. In general, such approximations are widespread in (behavioral) type theories and are in fact one of the key ingredients that make them decidable.

Several future research directions stem from this work. On the technical side, a limit of our technique is that bpel activities are "static", i.e. they cannot create other services on the fly. This constraint implies the finiteness of models and, for this reason, it is possible to effectively associate an abstract description to activities. However, this impacts on scalability, in particular when services adapt to peaks of requests by creating additional services. It is well-known that such an additional feature makes models to be infinite states and requires an approximate inferential process to extract abstract descriptions from activities. Said otherwise, extending our technique to full ccs or π-calculus amounts to defining abstract finite models such that Theorem 3.1 does not hold anymore. For this reason, under-and over-estimations for services and clients, respectively, must be provided.

Another interesting technical issue concerns the extension of our study to other semantics for bpel activities, such as the preorder in [START_REF] Bravetti | A theory of contracts for strong service compliance[END_REF], or even to weak bisimulation (which has a polynomial computational cost). To this aim, the axiomatizations that have been defined for these semantics might be used to select normal forms of processes and in turn to determine their contracts. However it is not clear whether such semantics admit a principal dual contract or not.

It is also interesting to prototyping our theory and experimenting it on some existing repository, such as http://www.service-repository.com/. To this aim we might re-use tools that have been already developed for the must testing, such as the concurrency workbench [START_REF] Cleaveland | The concurrency workbench: a semantics-based tool for the verification of concurrent systems[END_REF].

A. Proofs

Notation

In this section we use some additional yet fairly conventional notation.

• We let ≤ be the prefixing ordering relation between sequences of actions.

• We generalize the definition of actions(•) to sequences of actions so that actions(ϕ) is the set of actions occurring in ϕ. • We write ϕ for the sequence obtained from ϕ by swapping each action with the corresponding co-action.

• We write X α1•••αn ====⇒ if there exists X such that X α1 =⇒ • • • αn =⇒ X .
• We extend continuations to sequences of actions. Let X ϕ =⇒. If ϕ = ε, then X(ϕ) = X; if ϕ = αϕ , then X(ϕ) = X(α)(ϕ ).

• We generalize the convergence and diveregence predicates so that X↓ε if X↓ and X↓αϕ if X↓ and X α =⇒ X implies X ↓ϕ. We write X↑ϕ if not X↓ϕ.

• Many proofs rely on the "unzipping of derivations" [START_REF] Hennessy | Algebraic Theory of Processes[END_REF], which decomposes the interaction between two terms X and Y. In particular, let [START_REF] Hennessy | Algebraic Theory of Processes[END_REF] for a more detailed discussion.

X | N Y ε =⇒ X | N Y .
=⇒ Y are combined to produce X | N Y ε =⇒ X | N Y . See

Proof of Lemma 2.1

The proof of Lemma 2.1 is a simple adaptation of a similar result for ccs * [START_REF] Busi | On the expressive power of recursion, replication and iteration in process calculi[END_REF]. Proof. For an arbitrary activity P we inductively define the set D(P ) as follows: . By induction hypothesis we have that either there exists ϕ ≤ ϕ such that X (ϕ )↑ or X (ϕ )↓ and X (ϕ ) R Y (ϕ ). In the first subcase we conclude by taking ϕ = αϕ , because X(ϕ ) = X(αϕ ) = X (ϕ ). In the second subcase we conclude by observing that X(ϕ) = X (ϕ ) and Y(ϕ) = Y (ϕ ).

D(0) def = {0} D( i∈I α i ;P i ) def = { i∈I α i ; P i } ∪ i∈I D(P i ) D(P | A Q) def = {P | A Q | P ∈ D(P ), Q ∈ D(Q)} D(P ;Q) def = {P ; Q | P ∈ D(P )} ∪ D(Q) D( i∈I P i ) def = { i∈I P i } ∪ i∈I D(P i ) D(P * )
Theorem A.1 (Theorem 4.1). For every X and Y, the following statements are equivalent:

1. X Y; 2. X ∼ Y; 3. X ∼C Y; 4. X ∼A+C Y.
Proof. We show 1 ⇒ 2 and 2 ⇒ 1, the remaining implications are analogous since the proof does not depend on the syntax of activities/behaviors except for the availability of prefixes, internal and external choices, which are valid constructs for both activities and behaviors. =⇒ Y . From Lemma A.2 we deduce that either there exists ϕ ≤ ϕ such that X(ϕ )↑ or X(ϕ)↓ and X(ϕ) Y(ϕ). In the first case, using the hypothesis T X we conclude {e} = init(T(ϕ )) = init(T ). In the second case, suppose Y | N T ε -→. From the definition of coinductive compliance we have Y(ϕ)↓ and, from condition (2) of Definition 4.1, we know that there exists X such that X(ϕ)

• (1 ⇒ 2) Let T X
ε =⇒ X ε -→ and init(X ) ⊆ init(Y ). Then X | N T ε =⇒ X | N T ε
-→ and, using the hypothesis T X, we conclude {e} ⊆ init(T ).

• (2 ⇒ 1) Suppose X ∼ Y and X↓. Regarding condition (1) of Definition 4.1, suppose by contradiction Y↑, let a be a name that does not occur in X nor in Y and consider T def = e + a. Then T X but T Y, which contradicts the hypothesis X ∼ Y. Hence Y↓ and condition (1) is satisfied. Regarding condition (2) of Definition 4.1, let s 1 , . . . , s n be the ready sets of X (there are finitely many of them) and suppose that there exists r such that Y ⇓ r and s i ⊆ r for every 1 ≤ i ≤ n, that is there exists From Lemma A.2 we deduce that either there exist ϕ ≤ ϕ and X such that X ϕ =⇒ X ↑ or X(ϕ)↓ and X(ϕ) Y(ϕ). By zipping the computations starting from X and T, in the first subcase we can build an infinite computation

α i ∈ r i \ s for every 1 ≤ i ≤ n. Consider T def = n i=1 α i ; e.
| N T = Y 0 | N T 0 ε -→ Y 1 | N T 1 ε -→ • • • such that T i e -→
X | N T ε =⇒ X | N T |ϕ | ε -→ • • • , while in the second case we can find an X such that X ϕ =⇒ X ε -→ and init(X ) ⊆ init(Y n ).
In both cases we deduce X must T, which is absurd. In case (b), we distinguish two subcases: b1. there exists n such that Y n ↑ or T n ↑. Then using an argument similar to case (a), it is possible to show a contradiction for X must T.

b2. Y and T communicate infinitely often, that is the computation may be unzipped into

Y ϕ =⇒ and T ϕ =⇒,
where ϕ is infinite. It is easy to prove that, for every finite ϕ ≤ ϕ, there is X such that X ϕ =⇒ X . Therefore there exists an infinite computation of X | N T that transits in the same states T 0 , T 1 , . . . as the ones of Y | N T. This contradicts the hypothesis X must T.

(⇒) We prove that

R def = {(Y 1 , Y 2 ) | Y 1 must Y 2 } is a coinductive compliance. Let Y 1 R Y 2 and
(α) must T. Then Y 1 must e + α ; T. From the hypothesis Y 1 must Y 2 we deduce Y 2 must e+α ;T, therefore Y 2 (α) must T. We conclude Y 1 (α) R Y 2 (α) by definition of R.
Proof of Theorem 4.3 Lemma A.3. Let i : σ R j : τ where R is a coinductive compliance and τ ϕ =⇒ and actions(ϕ) ⊆ i. Then either there exists ϕ ≤ ϕ such that σ(ϕ )↑ or σ(ϕ)↓ and σ(ϕ) R τ (ϕ).

Proof. Analogous to that of Lemma A.2.

Theorem A.4 (Theorem 4.3).

is the largest coinductive subcontract relation.

Proof. We begin showing that is a coinductive subcontract relation. Suppose i : σ j : τ and σ↓. Then by Definition 4.3 we know i ⊆ j. We now prove the conditions of Definition 4.4 in order.

1. Suppose by contradiction that τ ↑. Then Ω σ and Ω τ , which contradicts the hypothesis i : σ j : τ , hence we conclude τ ↓ and condition (1) is satisfied. 2. Let r 1 , . . . , r n be the ready sets of σ and assume by contradiction that there exists s such that τ ⇓ s and for every 1 ≤ i ≤ n there exists α i ∈ r i \ s. By definition of ready set we have τ

ε =⇒ τ ε -→ and init(τ ) ⊆ s. Consider ρ def = 1≤i≤n α i ; e. Then, ρ σ but ρ τ because τ | N ρ ε =⇒ τ | N ρ ε -
→ and e ∈ init(ρ), which is absurd. Hence we conclude that r i ⊆ s for some 1 ≤ i ≤ n and condition (2) is satisfied. 3. Let τ α =⇒ and α ∈ i. It must be the case that σ α =⇒, otherwise e+α σ while e+α τ , which contradicts the hypothesis i : σ j : τ . Let ρ be an arbitrary behavior such that actions(ρ) \ {e} ⊆ i and ρ σ(α). Then e + α ; ρ σ. From the hypothesis i : σ j : τ we deduce e + α ;ρ τ , hence ρ τ (α). We conclude i : σ(α) j : τ (α) because ρ is arbitrary, hence condition (3) is satisfied.

Next we show that every coinductive subcontract relation is included in , proving that is indeed the largest one. Let i : σ R j : τ where R is a coinductive subcontract. By Definition 4.4 we know that i ⊆ j. Let k : ρ be such that k \ {e} ⊆ i and ρ σ. 1. If i : σ j : τ and i : σ j : τ , then i : σ j : τ ⊕ τ ; 2. if i : 0 j : τ , then i : σ j : σ + τ (width extension); 3. if i : 0 j : τ , then i : σ j : σ{ τ / 0 }, where σ{ τ / 0 } is the replacement of every occurrence of the contract name 0 with τ (depth extension).

Proof. We only show the proof of item (2), the others being simpler/analogous. Using Theorem 4.3, it is enough to show that R def = {(i : σ, j : σ + τ ) | i : 0 j : τ } ∪ {(i : σ, i : σ) | i : σ is an extended contract} is a coinductive subcontract. Since is obviously reflexive, the only interesting case to consider is when i : σ R j : σ + τ and i : 0 j : τ . From i : 0 j : τ we deduce i ⊆ j. Now suppose σ↓; we prove the conditions of Definition 4.4 in order:

1. From i : 0 j : τ we deduce τ ↓, hence σ + τ ↓. 2. Let σ + τ ⇓ r. Then there exist r 1 and r 2 such that σ ⇓ r 1 and τ ⇓ r 2 and r = r 1 ∪ r 2 . We conclude by observing that r 1 ⊆ r. Proof of Theorem 6.1

Theorem A.6 (Theorem 6.1). Let k : ρ be compliant with Γ 1 and Γ 2 be a refinement of Γ 1 . Then k : ρ is also compliant with Γ 2 .

Proof. Let Γ 1 = A (i 1 : σ 1 , . . . , i n : σ n ) and Γ 2 = A (j 1 : τ 1 , . . . , j n : τ n ) and consider a computation

Γ 2 | N ρ ε =⇒ Γ 2 | N ρ
where Γ 2 = A (j 1 : τ 1 , . . . , j n : τ n ). By unzipping this computation we deduce that there exists a sequence ϕ of actions such that ρ ϕ =⇒ ρ and Γ 2 ϕ =⇒ Γ 2 . By unzipping the computation of Γ 2 with respect to all of its participants we obtain n sequences ϕ 1 , . . . , ϕ n of actions such that τ i ϕi =⇒ τ i for every 1 ≤ i ≤ n. Note that ϕ is obtained by erasing pairs of complementary actions from the ϕ i 's, which correspond to synchronizations occurred within the choreography and solely pertain to names in A, and by suitably interleaving the remaining actions. Using i i : σ i j i : τ i , condition (2), and actions(ϕ) ⊆ k\{e} ⊆ actions(Γ 1 ), we deduce that all the actions in the ϕ i are in i i and σ i ϕi =⇒ for every 1 ≤ i ≤ n. By zipping these derivations we obtain that Γ 1 ϕ =⇒ as well. We proceed by considering the two possibilities in Definition 2.2. Suppose Γ 2 | N ρ ε -→. If there exists Γ 1 such that Γ 1 ϕ =⇒ Γ 1 and Γ 1 ↑, then from ρ Γ 1 we conclude {e} = init(ρ ). If Γ 1 ↓ whenever Γ 1 ϕ =⇒ Γ 1 , then from Γ 2 ε -→ we deduce that for every 1 ≤ i ≤ n there exists σ i such that σ i ϕi =⇒ σ i and init(σ i ) ⊆ init(τ i ). Take Γ 1 = A (i 1 : σ 1 , . . . , i n :

σ n ). Then Σ 1 | N ε =⇒ Σ 1 | N ρ ε
-→ and from ρ Σ 1 we conclude {e} ⊆ init(ρ ).

Suppose Γ 2 ↑. This may happen either because one (or more) participants diverge autonomously, or because two (or more) participants interact infinitely often. By definition of refinement and using the same arguments as above, we obtain that there exists Γ 1 such that Γ 1 ϕ =⇒ Γ 1 and Γ 1 ↑. From the hypothesis ρ Γ 1 we conclude {e} = init(ρ ).

Fig. 1 .

 1 Fig. 1. Summary of contributions.

Fig. 2 .

 2 Fig.2. bpel business process for an e-commerce service.

1 .

 1 (a ⊕ b | {a,b} a ⊕ b) ; c ε -→ (a | {a,b} a ⊕ b) ;c by (if), (flow), and (seq). By the same rules, it is possible to have (a | {a,b} a ⊕ b) ;c ε -→ (a | {a,b} b); c, which cannot reduce anymore (a | {a,b} b is a deadlocked activity). 2. let Ψ def = 0 ; (0 ⊕ 0) * . Then, according to rules (seq-end), (if), and (while), Ψ ε -→ Ψ and Ψ ε -→ 0.

3 .

 3 (a | {a} a) * ε -→ 0 | {a} 0 ; (a | {a} a) * by rules (link) and (while).

Lemma 2 . 1 .

 21 Let reach(P ) def = {Q | ∃ϕ : P ϕ =⇒ Q}. Then, for every activity P , the set reach(P ) is finite.

  For example, a ;e + b; e a ⊕ b and a; e ⊕ b; e a + b but a; e ⊕ b;e a ⊕ b because of the computation a ⊕ b | N a; e ⊕ b; e ε =⇒ b | N a ;e ε

  <process> <sequence> <receive partnerLink="e-commerce" operation="Login"/> <while> <condition> ... check credentials ... </condition> <sequence> <invoke partnerLink="e-commerce" operation="InvalidLogin"/> <receive partnerLink="e-commerce" operation="Login"/> </sequence> </while> <invoke partnerLink="e-commerce" operation="ValidLogin"/> ... </sequence> </process>

Fig. 4 .

 4 Fig. 4. bpel business process for an e-commerce service.

Example 3 .

 3 2.

  Figure 4 reports the initial fragment of the bpel code that implements the e-commerce service whose conversation is shown in Figure 3 and is discussed in Example 3.1. The e-commerce service is represented in abstract bpel as the process P defined by P def = Login ; (InvalidLogin ; Login) * ;ValidLogin ; Q According to the above definition, the contract associated to P is

Definition 4 . 1 .

 41 A coinductive compliance is a relation R such that X R Y and X↓ implies 1. Y↓, and 2. Y ⇓ r implies X ⇓ s for some s ⊆ r, and 3. Y α =⇒ implies X α =⇒ and X(α) R Y(α).

Theorem 4 . 2 .

 42 X must Y if and only if X ∼ Y.

  maximal, then ϕ = ϕ e and e does not occur in ϕ . For example {a, e} : a; e, {a} : C, where C = a ;C, and ∅ : Ω are canonical; {a, b, e} : a ;e + b and {a} : C , where C = a ⊕ C , are not canonical.

Definition 5 . 1 (

 51 Dual contract). Let k : ρ be a canonical extended contract. The dual of k : ρ is k \ {e} : D kρ where D k ρ is the contract name defined as follows:

C 1 =

 1 {a,a,e} a ;e = a; Ω + (0 ⊕ a; Ω). The dual of a divergent (canonical) client {a, e} : C, where C = a; e ⊕ C, is also well defined: D {a,e} C = a; Ω. We finally observe that the definition also accounts for duals of nonterminating clients, such as {a} : C , where C = a; C . In this case, D {a} C = a; D {a} C . Similarly to the definition of contract names C P in Section 3, it is possible to prove that D k ρ is well defined. Lemma 5.1. For every k : ρ, the set cnames(D k ρ ) is finite. Example 5.1. We illustrate the definition of dual of an extended contract on a potential client of the service in the Example 3.1. This simple client Logins and, when the credentials have been accepted, performs exactly one Query to the Catalog and then Logouts. The contract of such a client is defined by the following equations: Login ;C 2 C 2 = InvalidLogin ;C 1 + ValidLogin ;C 3 C 3 = Query ;C 4 C 4 = Catalog ;C 5 C 5 = Logout ;e Let k = {Login, InvalidLogin, ValidLogin, Query, Catalog, Logout, e} and notice that k : C 1 is canonical. Its principal dual extended contract is k \ {e} : D k C 1

Lemma A. 1 (

 1 Lemma 2.1). Let reach(P ) = {Q | there are µ 1 , . . . , µ n with P µ1 -→ • • • µn -→ Q}. Then, for every activity P , the set reach(P ) is always finite.

def= 1 Lemma A. 2 .

 12 {P * , 0} ∪ {P ;P * | P ∈ D(P )} A simple inductive argument allows one to establish that D(P ) is finite for every P . Now, we conclude if we are able to show that P µ -→ P implies D(P ) ⊆ D(P ). This follows from an induction on the derivation of P µ -→ P . We leave the details to the reader.Proof of Theorem 4.Let X R Y where R is a coinductive compliance and Y ϕ =⇒. Then either there exists ϕ ≤ ϕ such that X(ϕ )↑ or X(ϕ)↓ and X(ϕ) R Y(ϕ). Proof. By induction on ϕ. If X↑, then we conclude immediately by taking ϕ = ε. If X↓, then by definition of coinductive compliance we have Y↓. If ϕ = ε, then we conclude X(ϕ) R Y(ϕ). If ϕ = αϕ , then by definition of coinductive compliance we have X def = X(α) R Y(α) def = Y

  and consider a derivation of Y | N T ε =⇒ Y | N T . By unzipping this derivation we obtain a sequence ϕ of actions such that T ϕ =⇒ T and Y ϕ

  We have T X and T Y, which contradicts the hypothesis X ∼ Y. Hence there exists 1 ≤ i ≤ n such that s i ⊆ r and condition (2) is satisfied. Regarding condition (3) of Definition 4.1, suppose Y α =⇒ and suppose, by contradiction, that X α =⇒. Then e + α X and e + α Y, which contradicts the hypothesis X ∼ Y, hence X α =⇒. Now let T be an arbitrary activity/behavior such that T X(α) and consider T def = e + α ;T . We have T X hence, from the hypothesis X ∼ Y, we deduce T Y. This implies T Y(α), hence we conclude X(α) ∼ Y(α) because T is arbitrary, and condition (3) is satisfied. Proof of Theorem 3.1 Theorem A.2 (Theorem 3.1). P C P . Proof. By Theorem 4.1 it is sufficient to prove that R def = {(P, C P )} is a coinductive compliance. The proof that R -1 is also a coinductive compliance is similar. Let X R Y. Then X = P and Y = C P for some P . Suppose P ⇓ for otherwise there is nothing to prove. From the definition of C P we deduce C P ⇓, hence condition (1) of Definition 4.1 is satisfied. Now let C P ⇓ r. By definition of C P we have P ⇓ s with s ⊆ r, therefore condition (2) of Definition 4.1 is satisfied. Finally, suppose C P α =⇒. Then P α =⇒. By definition of R we have P (α) R C P (α) and we conclude that condition (3) of Definition 4.1 is satisfied by observing that C P (α) = C P (α) . Proof of Theorem 4.2 Theorem A.3 (Theorem 4.2). X must Y if and only if X ∼ Y. Proof. Because of Theorem 4.1 we can show the equivalence between must and . (⇐) Let X Y and assume, by contradiction, that X must T and Y must T for some T. Then there must be a maximal computation Y

  for every i = 0, 1, . . . . We distinguish two cases: (a) the computation is finite, (b) the computation is infinite. In case (a) there exists n such that Y n | N T n ε -→. Then there exists ϕ such that Y ϕ =⇒ Y n and T ϕ =⇒ T n .

  Consider a derivation of τ | N ρ ε =⇒ τ | N ρ . By unzipping this derivation we obtain a sequence ϕ of actions such that ρ ϕ =⇒ ρ and τ ϕ =⇒ τ and furthermore actions(ϕ) ⊆ i.From Lemma A.3 we deduce that either there exists ϕ ≤ ϕ such that σ(ϕ )↑ or σ(ϕ)↓ and σ(ϕ) R τ (ϕ). In the first case, using the hypothesis ρ σ we conclude {e} = init(ρ(ϕ )) = init(ρ ). In the second case, suppose τ | N ρ ε -→. From the definition of coinductive subcontract we have τ (ϕ)↓ and, from condition (2) of Definition 4.4, we know that there exists σ such that σ(ϕ)ε =⇒ σ ε -→ and init(σ ) ⊆ init(τ ). Then σ | N ρ ε =⇒ σ | N ρ ε -→and, using the hypothesis ρ σ, we conclude {e} ⊆ init(ρ ). Proofs of Propositions 4.1 and 4.2 Proposition A.1 (Proposition 4.1). The following properties hold:

3 . 2 def= 1 Theorem A. 5 (

 3215 Let σ + τ α =⇒ and α ∈ i. From i : 0 j : τ we deduce τ α =⇒, hence (σ + τ )(α) = σ(α). We conclude σ(α) R σ(α) by definition of R. Proposition A.2 (Proposition 4.2). i : σ ≈ j : τ if and only if σ τ and i = j. Proof. Using Theorems 4.1 and 4.3 it is enough to show that R 1 def = {(σ, τ ) | i : σ i : τ } and R {(i : σ, i : τ ) | σ τ } respectively are a coinductive compliance and a coinductive subcontract. The result follows easily from Definitions 4.1 and 4.4.Proof of Theorem 5.Theorem 5.1). Let k : ρ be a canonical extended contract. Then:1. ρ D k ρ ; 2. if k \ {e} ⊆ s and ρ σ, then k \ {e} : D k ρ s : σ.Proof. Regarding item 1, we remark that, by definition of dual, every derivationD k ρ | N ρ ε =⇒ σ | N ρ may be rewritten into D k ρ | N ρ ε =⇒ D k ρ(ϕ) | N ρ ε =⇒ σ | N ρ , where ρ(ϕ) ε =⇒ ρ and D k ρ(ϕ) ε =⇒ σ. If σ↑, then D k ρ(ϕ) = Ω,which means that {e} = init(ρ ). In this case, the conditions in Definition 2.2 are satisfied. If σ | N ρ ε -→, then assume by contradiction that e ∈ init(ρ ). By definition of canonical client, init(ρ ) = ∅. Therefore, by definition of dual, D k ρ(ϕ) ⇓ r implies r = ∅ because D k ρ(ϕ) has an empty ready set provided every ready set of ρ(ϕ) contains e, which is not the case by hypothesis. Hence we conclude init(σ) = ∅ and init(ρ ) ∩ init(σ) = ∅ by definition of dual, which is absurd by σ | N ρ ε -→. Regarding item 2, let k def = k \ {e} and let R be the least relation such that: • if σ ϕ =⇒, ρ ϕ =⇒, and σ↓ϕ, then k : D k ρ(ϕ) R s : σ(ϕ); • if σ ϕ =⇒ and either ρ ϕ =⇒ or σ↑ϕ, then k : Ω R s : σ(ϕ). Note that k : D k ρ R s : σ. Indeed, if σ↑, then from ρ σ we derive init(ρ) = {e}, hence D k ρ = Ω by definition of dual. Using Theorem 4.3 it suffices to prove that R is a coinductive subcontract. Let k : D k ρ(ϕ) R s : σ(ϕ) and D k ρ(ϕ) ↓. The conditions of Definition 4.4 are proved in order: 1. By definition of R we have σ↓ϕ, hence σ(ϕ)↓.

2 .

 2 Assume σ(ϕ) ⇓ r. Let {s 1 , . . . , s n } def = {s | ρ(ϕ) ⇓ s, e ∈ s}. From ρ σ we derive s i ∩ r = ∅ for every 1 ≤ i ≤ n, namely there exists α i ∈ s i ∩ r for every 1 ≤ i ≤ n. By definition of dual we have D k ρ(ϕ) ⇓ {α 1 , . . . , α n } and we conclude by observing that {α 1 , . . . , α n } ⊆ r. 3. Let σ(ϕ) α =⇒ and α ∈ k . Then α ∈ k and D k ρ(ϕ) α =⇒ by definition of dual. If ρ(ϕ) α =⇒, then D k ρ(ϕ) (α) = Ω and we conclude k : Ω R σ(ϕα) by definition of R. If ρ(ϕ) α =⇒, then we distinguish two subcases: either (i) σ(ϕα)↑ or (ii) σ(ϕα)↓. In subcase (i), from ρ σ we derive init(ρ(ϕα)) = {e}, hence D k ρ(ϕα) = Ω and k : Ω R s : σ(ϕα) by definition of R. In subcase (ii) we have D k ρ(ϕ) (α) = D k ρ(ϕα) and we conclude k : D k ρ(ϕ) (α) R s : σ(ϕα) by definition of R.

Table 1 .

 1 Syntax of bpel abstract activities.

P, Q, P i

Table 2 .

 2 Legend for the operations of the bpel process in Figure2.

	Name Operation
	sPO	sendPurchaseOrder
	rS	requestShipping
	sS	sendSchedule
	iPC	initiatePriceCalculation
	sSP	sendShippingPrice
	sI	sendInvoice
	rPS	requestProductionScheduling
	sSS	sendShippingSchedule
	sti	ship-to-invoce
	sts	ship-to-scheduling
	and P 1 ⊕ • • • ⊕ P

n , respectively.

Table 2 :

 2 sPO ; rS ; (sti | ∅ sS ;sts) | {sti} iPC ; sti ;sSP ; sI | {sts} rPS ; sts ; sSS ; sPO

Table 3 .

 3 Operational semantics of abstract bpel

		(while)
	end) P * ε -→ 0	P P * µ -→ P µ -→ P ; P *

  It is relevant to ask whether this implementation of the e-commerce service is equivalent to the previous one according to the compliance pre-order. It turns out that this is not the case, in particular the client activity For example, after the two operations sPO and rPS, the first test reduces to 0, which allows no further synchronizations with the service and does not perform e actions. It can be shown that (1) is compliant-equivalent to the abstract activity

Example 2.2. As a counter-example of compliance, consider the process sPO ; rS ; (sS | ∅ rPS); sSS | ∅ iPC ; sSP ; sI ;sPO (2) which has been obtained from Example 2.1 by removing and serializing the synchronizations described by the links. sPO ; (e + rPS) is compliant with (2) but not with (1), while the client activity sPO ; rPS ; e is compliant with (1) but not with (2). sPO ; rS ; (sS | ∅ rPS); sSS | ∅ iPC ; sSP ; sI + rPS ; rS ;(sS ;sSS | ∅ iPC ; sSP ; sI) ; sPO

  Then, by definition of | N , there is a sequence ϕ

	of actions such that X	ϕ =⇒ Y . By "zipping" we mean the inverse process whereby two
	derivations X

ϕ =⇒ X and Y ϕ =⇒ X and Y ϕ

  Y 1 ↓. We prove the three conditions of Definition 4.1 in order.1. Suppose by contradiction Y 2 ↑. Then Y 1 must e ⊕ e whereas Y 2 must e ⊕ e which is absurd, hence Y 2 ↓. 2. Let r 1 , . . . , r n be the ready sets of Y 1 . Assume by contradiction that there exists s such that Y 2 ⇓ s and r i ⊆ r for every 1 ≤ i ≤ n. That is, every r i is nonempty and, for every 1 ≤ i ≤ n, there existsα i ∈ r i \ s. Now Y 1 must 1≤i≤n α i ;e while Y 2 must 1≤i≤n α i ; e, which is absurd. 3. Let Y 2 α =⇒ Y 2 . Then also Y 1 α =⇒.In fact, if this were not the case, then Y 1 must e+α while Y 2 must e+α, which is absurd. Let T be an arbitrary term such that Y 1

 [START_REF] Abramsky | The lazy lambda calculus[END_REF]The research reported in this paper was partially funded by the EU FP7 610582 project called ENVISAGE.