Formal Commercial Contracts

Work in Progress

Christian Stefansen

Department of Computer Science, University of Copenhagen

(joint work with Jesper Andersen, Ebbe Elsborg, Fritz Henglein, and Jakob Grue Simonsen)

Presentation at Microsoft Research, Redmond, June 14, 2004

Formal Commercial Contracts cstef@diku.dk

Agenda

• Motivation

• Definitions and Focus

• The REA Model

• Our Contract Model

• Syntax and Semantics

• Contract Analysis

The NEXT Project

Next Generation Software Technology for Enterprise Systems (since 2001)

Partners:

• Microsoft Business Solutions, formerly Navision A/S

• IT University of Copenhagen: Founded 1999, 40 full-time researchers, active broadly in IT (mathematical-technical, design and business) research; see http://www.it.edu

• Department of Computer Science, University of Copenhagen (DIKU): Founded 1970, 30 full-time researchers, active in CS (algorithmics, distributed systems, information systems/HCI, computer vision, programming languages etc.) research; see http://www.diku.dk

Project homepage: http://www.it.edu/next/

Formal Commercial Contracts cstef@diku.dk

What is a Contract?

An agreement to do or not do certain things. Used by (almost) any company in daily operation. Any exchange is governed by a written or oral agreement or the underlying context and legislation.

Formal Commercial Contracts cstef@diku.dk

Background

• Capturing contractual obligations is important for planning and reporting.

• Monitoring/execution, analysis, and integration not or badly supported in present ERP (Enterprise Resource Planning) systems.

Background

Problems associated with informal contract handling in practice:

• Disagreement on what events have happened

• Disagreement on semantics of contract

• Potential disagreement on residual contract (due to nondeterminacy of consequences)

• Malexecution of contracts

• Entering bad contracts due to impossible or inferior analysis

• Reporting the state of company affairs (current commitments, capacity requirements, risk analysis, valuation, due diligence) is not feasible due to contracts in natural language stored in paper.

Goals

A domain-specific contract specification language addressing the current problems above by giving:

• Flexible user-specified contracts

• Automatic contract execution (less work-intensive, larger degree of non-repudiation)

• Deadline management (integration with workflow systems and ERP systems)

• (Real-time) reporting on active contracts

• Contract analysis (valuation, capacity requirements, risk analysis)

• Contract design support (identifying race conditions, non-determinism)

Focus

The primary focus is on “happy path” actualization of valid going-concern contracts between two or more disjoint parties

Happy path A “good faith” intended execution path of a contract. A course of action that complies with the purpose, intent, and “meeting of minds” of the contract.

Example Contract # 1

Abbreviated agreement of sale:

Agreement to Sell Goods Section 1. Seller shall sell and deliver to buyer (description of goods) no later than (date). Section 2. In consideration hereof, buyer shall pay (amount in dollars) in cash on delivery.

This describes a basic micro-economic phenomenon, namely, an exchange between economic agents of scarce economic resources that have utility.

REA Definitions (McCarthy, 1982) ^{1}

Economic Resource Economic resource are defined by Ijiri [1975, pp. 51-2] to be objects that (1) are scarce and have utility and (2) are under the control of an enterprise. In practice, the definition of this entity set can be considered equivalent to that given the term “asset” by the FASB [1979, pp. 51-7] with one exception: economic resources in the schema do not automatically include claims such as accounts-receivable.

Economic Agent Economic agents are “identifiable parties with discretionary power to use

or dispose of economic resources”. Economic Event Economic events are defined by Yu [1976, p. 256] as “a class of

phenomena which reflects changes in scarce means [economic resources] resulting from production, exchange, consumption, and distribution.”

The REA has an independent perspective as opposed to the trading partner perspective.

1Proposed as an alternative to double-entry bookkeeping (it is easily shown that there are several maps from the REA model to the traditional ledger).

Contract Example #2: Legal Services

Abbreviated legal services contract:

Agreement to Provide Legal Services Section 1. The attorney shall provide, on a non-exclusive basis, legal services up to (n) hours per month, and furthermore provide services in excess of (n) hours upon agreement. Section 2. In consideration hereof, the company shall pay a monthly fee of (amount in dollars) before the 8th day of the following month and (rate) per hour for any services in excess of (n) hours 40 days after the receival of an invoice. Section 3. This contract is valid 1/1-12/31, 2004.

Patterns in Contracts

Contracts are composed of following “patterns”:

• Specific commitments for the transmission of money, goods or services by whom to whom.

• Sequential execution of subcontracts (services first, payment later)

• Choices between subcontracts, in particular options (excess hours)

• Concurrent execution of subcontracts (each month)

• Repetition of subcontracts (repetion of monthly service)

• Time constraints (in particular deadlines) on individual commitments and whole (sub)contracts.

Formal Commercial Contracts cstef@diku.dk

Real-Life Contracts

We analyzed the domain of commercial contracts by considering 15 standard contracts:

Agreement to Sell Goods  Sale with Installment Payment
General Contract  Agreement to Sell
Balloon Note  Contractor Agreement
Legal Services Agreement  The Danish Trade Law (Købeloven)
Website Development Contract Lease Contract
Loan and Security Agreement  License Agreement
Operating Agreement  Supply Agreement

Manufacturing Agreement

Observations from the 15 Contracts

(⋆ = Primary focus)

• Contracts have these main components: – Definitions

– Structural description (processes) ⋆

– Conditions on specific parts

– Conditions on all parts

– Specification of remedies

• Contract path is decided by four choice types: – Agents actively choose ⋆

– Time chooses (say, an option expires)

– Observables (cf. Peyton Jones/Eber) choose

– Log of events chooses

Contract specification is very similar to protocol specification for networked systems.

Formal Commercial Contracts cstef@diku.dk

Domain-specific languages

Goal: Capture contract patterns in domain-specific language Hypothesis: DSL based on above contract patterns alone good basis for contract specification Method for testing hypothesis:

• analysis of adequacy in application domain

• semantics-driven design and analysis of language

Atomic Contracts and Combinators

Success/Failure

The succeeded/failed contract with no commitments. transmit (A_{1}, A_{2}, R, T |P).c

The commitment of agent A_{1} to transmit resource R to agent A_{2} at time T subject to predicate P. ;

A sequence of two contracts. Only when the first contract is reduced to Success can the execution of the next begin.

∥

The parallel and independent execution of two contracts. +

The (non-deterministic) choice of exactly one of two contracts. f(a⃗)

The expansion to a named contract f with concrete arguments a⃗. letrec f_{i}[X⃗_{i}] = c_{i} in c

Contract c with named contracts f_{i} with formal arguments X_{i} bound to c_{i}.

Example Contract #1: Sale of Goods

letrec
  sale [seller, buyer, goods, payment, t1, t2] =
           transmit (seller, buyer, goods, T | T < t1)
        || transmit (buyer, seller, payment, T | T < t2)
in
  sale ("McD", "Me", "Burger", 4 Euros, 7/1, 7/1)

Example Contract #2: Legal Services

letrec
legal [lawyer, comp, hours, payment, extraprice, end, n] =
   (Success
     + transmit(lawyer, comp, H, T | n <= T and T < min(end,nextmonth(n))));
   (legal (lawyer, comp, hours, payment, extraprice, end, nextmonth(n))
     + Success)
|| transmit(comp,lawyer, payment, T | T <= nextmonth(n) + 10)
|| (transmit(lawyer, comp, invoice, T1 | obs(hoursspent,n) > hours and
                  (invoice.total = obs(hoursspent,n) - hours) * extraprice)
     .transmit(comp, lawyer, invoice.total, T2 | T2 <= T1 + 45)
     + Success)
in
legal ("Lawyer X", "Me", 20, 10000 Euros, 1200 Euros, 12/31, 1/1)

Formal Commercial Contracts cstef@diku.dk

(Part of) The Denotational Semantics

Trace tr a finite sequence of events Contract C a set of traces

C[[Success]]^{γ;ρ} = {⟨⟩}
C[[Failure]]^{γ;ρ} = ∅
C[[transmit(A_{1}, A_{2}, R, T | P). c]]^{γ;ρ} = {(a_{1}, a_{2}, r, t) s : (a_{1}, a_{2}, r, t) ∈ E, s ∈ Tr |
R[[P]]^{ρ} = true ∧ s ∈ C[[c]]^{γ;ρ,A1↦a1,A2↦a2,R↦r,T ↦t}
C[[c_{1} + c_{2}]]^{γ;ρ} = C[[c_{1}]]^{γ;ρ} ∪ C[[c_{2}]]^{γ;ρ}
C[[c_{1} ∥ c_{2}]]^{γ;ρ} = \{s | ∃s_{1} ∈ C[[c_{1}]]^{γ;ρ}, s_{2} ∈ C[[c_{2}]]^{γ;ρ}. ( \begin{matrix}s_{1} \\ s_{2} \end{matrix} ) ⇝ s\}
C[[c_{1}; c_{2}]]^{γ;ρ} = {s_{1}s_{2} | s_{1} ∈ C[[c_{1}]]^{γ;ρ} ∧ s_{2} ∈ C[[c_{2}]]^{γ;ρ}}

Basic Questions

Residual contract C/s The residual rights and obligations of C after s has been executed.

Basic questions we want answered, given C and s:

• Is C/s nullable, that is completed or possibly completed successfully?

• Is C/s consistent (not necessarily completed, but can still be extended to a performaing trace s′), or is C/s inconsistent (s cannot be extended to a performing trace by any trace s′.)

• Given consistent C/s, is C/se consistent (e is compliant) or inconsistent (e is a breach of contract)?

Formal Commercial Contracts cstef@diku.dk

Approach: Reduction Semantics

Define reduction semantics C ⟶^{e} C′, such that C′ (in our language) represents C/e. Extends to C ⟶^{s} C′. Then answer above:

• Is C′ equivalent with Success + C′′ for some C′′?

• Is C′ equivalent with Failure or is it not?

• If C ⟶^{e} C′, is C′ equivalent with Failure? Advantage: Any analysis of contracts automatically extends to analysis of partially executed contracts.

Formal Commercial Contracts cstef@diku.dk

Event Model

Figure 1: Contract Processing Module

Assume events and commitments match one-to-one. We use a discrete time model. Granularity can be chosen arbitrarily. Assume events arrive in ascending time order.

Presentation at Microsoft Research, Redmond, June 14, 2004 21 Formal Commercial Contracts cstef@diku.dk

Example Contract #1 Revisited: Sale of Goods

Contract reduction using events:

           transmit (seller, buyer, goods, T | T < 7/1)
        || transmit (buyer, seller, 100, T | T < 8/1)
(seller, buyer, goods, 1/1) ->
           Success
        || transmit (buyer, seller, 100, T | T < 8/1)
(buyer, seller, 100, 7/19) ->
           Success
        || Success

Formal Commercial Contracts cstef@diku.dk

Example Contract #3 (Compact Notation)

Contract reduction using events:

     ((t1 + Success);t2) || t2.t3
-e2->
     Success || t2.t3
-e3->
     Fail

Reduction is non-deterministic!

Formal Commercial Contracts cstef@diku.dk

Non-determinism

Remedies in practice:

• Dynamically generated identifiers such as invoice numbers (intuitively corresponding to “tagging” of commitments) to determinize matching.

• Manual “matching” performed by bookkeepers, ensuing discrepancies and disagreements between partners resolved by “backtracking”.

Remedy in semantics:

• Explicit tagging of commitments (see Andersen/Elsborg, 2003) or explicit representation of “routing” of event to target commitment

• Backtracking semantics: Deterministic semantics C ⟶^{e} C′ such that C/e = C′. (In nondeterministic semantics: if C ⟶^{e} C′ then C′ ⊆ C/e

Formal Commercial Contracts cstef@diku.dk

Reduction with Explicit Control

     ((t1 + Success);t2) || t2.t3
-e2,r->
     ((t1 + Success);t2) || t3
-e3,r->
     ((t1 + Success);t2) || Success

Formal Commercial Contracts cstef@diku.dk

Reduction with Backtracking

((t1 + Success);t2) || t2.t3
-e2->
(Success || t2.t3) + (((t1 + Success);t2) || t3)
-e3->
Fail + (((t1 + Success);t2) || Success)

Formal Commercial Contracts cstef@diku.dk

Some Rules from the Reduction Semantics (Backtracking)

D, ρ ⊢_{D} Success ⟶^{e} Failure D, ρ ⊢_{D} Failure ⟶^{e} Failure

\frac{ρ ⊧ P [e/X⃗]}{D, ρ ⊢_{D} transmit(X⃗ | P). c ⟶^{e} c[e/X⃗]}

\frac{D ⊢ c nullable D, ρ ⊢_{D} c ⟶^{e} d D, ρ ⊢_{D} c′ ⟶^{e} d′}{D, ρ ⊢_{D} c; c′ ⟶^{e} d; c′ + d′}

\frac{D ⊬ c nullable D, ρ ⊢_{D} c ⟶^{e} d D, ρ ⊢_{D} c′ ⟶^{e} d′}{D, ρ ⊢_{D} c; c′ ⟶^{e} d; c′}

Formal Commercial Contracts cstef@diku.dk

Multiple Unfoldings

     f[t] = transmit(a,b,r,t) || f(t)

En event (a, b, r, t) can match any of the infinitely many parallel transmits. The denotation of the contract is ∅. Contracts should be guarded to prevent infinite unfolding. Intuitively, a contract is guarded iff recursive unfolding is guarded by commitments.

D ⊢ Success guarded D ⊢ Failure guarded D ⊢ transmit(X⃗ | P). c guarded

\frac{D ⊬ c nullable D ⊢ c guarded}{D ⊢ c; c′ guarded}  \frac{D ⊢ c nullable D ⊢ c guarded D ⊢ c′ guarded}{D ⊢ c; c′ guarded}

Formal Commercial Contracts cstef@diku.dk

Contract Analysis: Task List and Next Point of Interest

Given a portfolio of running contracts, an agent needs to know:

• What commitments and choices are ready to be executed by the agent?

• When is the next time a contract changes (say, a deadline expires)?

Formal Commercial Contracts cstef@diku.dk

Predicate Languages

Consider a simply predicate language with expressions on the form [a;b], where a, b ∈ ℝ ∪ {−∞, ∞}. An expression [a;b] is valid iff a ≤ b. Given a time t the predicate [a; b] is true if and only if t ∈ [a; b].

Task List

fun tasks a t Success      = []
| tasks a t Fail         = []
| tasks a t
  transmit(a1,a2,r,t|[a;b]).c = if a = a1 andalso t in [a;b]
                                     then [trans(a1,a2,r,t|[a;b])]
                                     else []
| tasks a t (c1 + c2)   = choose(tasks a t c1, tasks a t c2)
| tasks a t (c1 ; c2)   = if nullable c1
                              then if tasks a t c1 <> []
                                   then choose(tasks a t c1, tasks a t c2)
                                   else tasks a t c2
                              else tasks a t c1
| tasks a t (c1 || c2)  = (tasks a t c1) @ (tasks a t c2)
| tasks a t (f a)        = tasks a t (expand f a)

Next Point of Interest (NPOI)

fun npoi t Success      = INF
| npoi t Fail         = INF
| npoi t
  transmit(a1,a2,r,t|[a;b]).c = if t <= a then a else
                                     if t <= b then b else INF
| npoi t (c1 + c2)   = min(npoi t c1, npoi t c2)
| npoi t (c1 ; c2)   = min(npoi t c1, if nullable c1
                                           then npoi t c2 else INF)
| npoi t (c1 || c2)  = min(npoi t c1, npoi t c2)
| npoi t (f a)        = npoi t (expand f a)

Analysis Example: Legal Services

Status of (guarded) legal services contract C on 2/4:

   (transmit (lawyer, lawyer, nohours, T | [3/1;3/1])
     + transmit(lawyer, comp, 20, T | [2/1;3/1]));
   (legal (lawyer, comp, hours, payment, extraprice, end, nextmonth(n))
     + Success)
|| transmit(comp, lawyer, payment, T | [3/1;3/11])
|| (transmit(lawyer, comp, invoice, T1 | [3/1;inf])
     .transmit(comp, lawyer, invoice.total, T2 | [T1;T1+45]) + Success)
|| transmit(comp, lawyer, payment, T | [2/1;2/11])
|| transmit(comp, lawyer, invoice.total, T2 | [2/3;3/18])
tasks 2/4 comp C =
     [transmit(comp, lawyer, payment, T | [2/1;2/11]),
      transmit(comp, lawyer, invoice.total, T2 | [2/3;3/18])]
npoi 2/4 C = 2/11

More Contract Analyses

• Account payable/accounts receivable

• Termination: (a) earliest termination (b) latest termination

• Check for no race conditions

• Deadlock

• Valuation (with respect to some agent A)

• Inventory line, supply requirement, resource flow profile (optimistic/pessimistic) - forecasting, supply-chain management

• General model checking for business rules: (a) static (b) dynamic/runtime (Timed LTL checking)

Discussion

• Good fit to domain despite language paucity

• Separation of predicate language and contract language seems good

• Event model should perhaps include other event types (e.g. timer events)

• Further experience with predicate layer is desirable

• Exploitation of algebraic properties using denotational model should be explored further

Formal Commercial Contracts cstef@diku.dk

Related Work

William McCarthy: Contract state machine Peyton Jones/Eber: Compositional contracts (only trading partner perspective) Formal calculi: π-Calculus, CSP (Communicating Sequential Processes) Many standardization initiatives: BPEL4WS, CrossFlow, UEML, etc.

Extensions

• Consider business rules (policies), perhaps using timed LTL or a contract “overlaying” operator

• Assume events and commitments do not match one-to-one

• User interface using a simple, tabular form

Contracts Not Considered

Some contract types and why they were left out:

• Employment agreements, severance, retirement plans require non-static agents regarded dually as separate parties and employees.

• Non-disclosure agreements, codes of ethics impose conditions on all existing contracts simultaneously and specify things not to do in an often subjective manner.

• Arbitration, remedies, and trade laws require the encoding of a large body of statutes and a fairly involved exception handling mechanism.

• Chapter 11s, separation, partnerships, bankruptcy, mergers, acquisitions modify the structure of the enterprise.

• Legal haggles (lawsuit, counter-suit, settlements) are subjective

Contract Process

Five phases (ISO OpenEDI, Part 1, 2003; Part 4, 2004; UBAC):

1. Planning

2. Identification

3. Negotiation

4. Actualization

5. Post-actualization

Formal Commercial Contracts cstef@diku.dk

Syntax for Contract Specifications

Γ; Δ ⊢ Success : Contract  Γ; Δ ⊢ Failure : Contract
\frac{Γ(f) = τ⃗ → Contract Δ ⊢ a⃗ : τ⃗}{Γ; Δ ⊢ f(a⃗) : Contract}  \frac{Δ′ = Δ, A_{1} : Agent, A_{2} : Agent, R : Resource, T : Time Γ; Δ′ ⊢ c : Contract Δ′ ⊢ P : Boolean}{Γ; Δ ⊢ transmit(A_{1}, A_{2}, R, T | P). c : Contract}
\frac{Γ; Δ ⊢ c_{1} : Contract Γ; Δ ⊢ c_{2} : Contract}{Γ; Δ ⊢ c_{1} + c_{2} : Contract}  \frac{Γ; Δ ⊢ c_{1} : Contract Γ; Δ ⊢ c_{2} : Contract}{Γ; Δ ⊢ c_{1} & c_{2} : Contract}
\frac{Γ; Δ ⊢ c_{1} : Contract Γ; Δ ⊢ c_{2} : Contract}{Γ; Δ ⊢ c_{1} ∥ c_{2} : Contract}  \frac{Γ; Δ ⊢ c_{1} : Contract Γ; Δ ⊢ c_{2} : Contract}{Γ; Δ ⊢ c_{1}; c_{2} : Contract}

\frac{Γ = \{f_{i} ↦ τ_{i1} × … × τ_{ini} → Contract\}_{i=1}^{m} Γ; Δ, X_{i1} : τ_{i1}, …, X_{ini} : τ_{ini} ⊢ c_{i} : Contract}{Δ ⊢ \{f_{i}[X⃗_{i}] = c_{i}\}_{i=1}^{m}\} : Γ}

\frac{Δ ⊢ \{f_{i}[X⃗_{i}] = c_{i}\}_{i=1}^{m} : Γ Γ; Δ ⊢ c : Contract}{Δ ⊢ letrec \{f_{i}[X⃗_{i}] = c_{i}\}_{i=1}^{m} in c : Contract}

Formal Commercial Contracts cstef@diku.dk

Denotational Semantics

Dom[[Boolean]] = {true, false}
Dom[[Agent]] = A
Dom[[Resource]] = R
Dom[[Time]] = T
E = A × A × R × T
Tr = E^{∗}
Dom[[Contract]] = 2^{Tr}
Dom[[τ_{1} × … × τ_{n} → Contract]] = Dom[[τ_{1}]] × … × Dom[[τ_{n}]] → 2^{Tr}

C[[Success]]^{γ;ρ} = {⟨⟩}
C[[Failure]]^{γ;ρ} = ∅
C[[f(a⃗)]]^{γ;ρ} = γ(f)(R[[a⃗]]^{ρ})
C[[transmit(A_{1}, A_{2}, R, T | P). c]]^{γ;ρ} = {(a_{1}, a_{2}, r, t) s : (a_{1}, a_{2}, r, t) ∈ E, s ∈ Tr |

R[[P]]^{ρ} = true ∧ s ∈ C[[c]]^{γ;ρ,A1↦a1,A2↦a2,R↦r,T ↦t}

C[[c_{1} + c_{2}]]^{γ;ρ} = C[[c_{1}]]^{γ;ρ} ∪ C[[c_{2}]]^{γ;ρ}
C[[c_{1} & c_{2}]]^{γ;ρ} = C[[c_{1}]]^{γ;ρ} ∩ C[[c_{2}]]^{γ;ρ}
C[[c_{1} ∥ c_{2}]]^{γ;ρ} = \{s | ∃s_{1} ∈ C[[c_{1}]]^{γ;ρ}, s_{2} ∈ C[[c_{2}]]^{γ;ρ}. ( \begin{matrix}s_{1} \\ s_{2} \end{matrix} ) ⇝ s\}
C[[c_{1}; c_{2}]]^{γ;ρ} = {s_{1}s_{2} | s_{1} ∈ C[[c_{1}]]^{γ;ρ} ∧ s_{2} ∈ C[[c_{2}]]^{γ;ρ}}
D[[{f_{i}[X⃗_{i}] = c_{i}}_{i=1}^{m}}]]^{ρ} = least γ : γ = {f_{i} ↦ λx⃗_{i}.C[[c_{i}]]^{γ;ρ,X⃗i↦x⃗i}}_{i=1}^{m}
C[[letrec \{f_{i}[X⃗_{i}] = c_{i}\}_{i=1}^{m} in c]]^{ρ} = C[[c]]^{D[[\{fi[X⃗i]=ci\}{m \atop i=1}\}]]ρ;ρ}

Residuation

We wish to monitor contracts as events come in and determine if events are performing or non-performing. If an event is performing, we must be able to find the remainder of the contract (henceforth the residual contract).

C[[c/e]]^{γ;ρ} = {s′ : s′ ∈ Tr | es′ ∈ C[[c]]^{γ;ρ}}

Let us write D, ρ ⊧ c = c′ if C[[c]]^{γ;ρ} = C[[c′]]^{γ;ρ} where γ = D[[D]]^{ρ}.

Formal Commercial Contracts cstef@diku.dk

Residuation Equalities

D ⊧ Success/e = Failure D ⊧ Failure/e = Failure

D ⊧ f(a⃗)/e = c[a⃗/X⃗]/e if(f[X⃗] = c) ∈ D

D ⊧ transmit(A_{1}, A_{2}, R, T | P). c/(a_{1}, a_{2}, r, t) = \{ \begin{matrix}c[a_{1}/A_{1}, a_{2}/A_{2}, r/R, t/T] & ifR[[P]]^{∅} = true \\ Failure & otherwise \end{matrix}

D ⊧ (c_{1} + c_{2})/e = c_{1}/e + c_{2}/e

D ⊧ (c_{1} & c_{2})/e = c_{1}/e & c_{2}/e
D ⊧ (c_{1} ∥ c_{2})/e = c_{1}/e ∥ c_{2} + c_{1} ∥ c_{2}/e

D ⊧ (c_{1}; c_{2})/e = \{ \begin{matrix}c_{1}/e; c_{2} + c_{2}/e & ifc_{1} contains ⟨⟩ \\ c_{1}/e; c_{2} + & otherwise \end{matrix}

Formal Commercial Contracts cstef@diku.dk

Guarded Contracts

To prevent uncontrolled unfolding and infinite residuation, we introduce guarding. Intuitively, a contract is guarded iff unfolding is guarded by commitments. (Analogously, if FIRST() set computation terminates.)

f[a] = transmit(a1,a2,r,t|true) || f(a+1) is not guarded
f[a] = transmit(a1,a2,r,t|true); f(a+1) is guarded

(Exercise for the audience: what is wrong with both contracts?)

Formal Commercial Contracts cstef@diku.dk

Guarded Contracts

D ⊢ Success guarded D ⊢ Failure guarded

D ⊢ transmit(X⃗ | P). c guarded

\frac{D ⊢ c guarded (f[X⃗] = c) ∈ D}{D ⊢ f(a⃗) guarded}  \frac{D ⊢ c guarded D ⊢ c′ guarded}{D ⊢ c + c′ guarded}
\frac{D ⊢ c guarded D ⊢ c′ guarded}{D ⊢ c & c′ guarded}  \frac{D ⊢ c guarded D ⊢ c′ guarded}{D ⊢ c ∥ c′ guarded}
\frac{D ⊬ c nullable D ⊢ c guarded}{D ⊢ c; c′ guarded}  \frac{D ⊢ c nullable D ⊢ c guarded D ⊢ c′ guarded}{D ⊢ c; c′ guarded}
\frac{D ⊢ c guarded}{⊢ letrec D in c guarded}

Presentation at Microsoft Research, Redmond, June 14, 2004 47

Formal Commercial Contracts cstef@diku.dk

Nullable Contracts

D ⊢ Success nullable \frac{D ⊢ c nullable (f[X⃗] = c) ∈ D}{D ⊢ f(a⃗) nullable}

\frac{D ⊢ c nullable}{D ⊢ c + c′ nullable}  \frac{D ⊢ c′ nullable}{D ⊢ c + c′ nullable}
\frac{D ⊢ c nullable D ⊢ c′ nullable}{D ⊢ c & c′ nullable}  \frac{D ⊢ c nullable D ⊢ c′ nullable}{D ⊢ c ∥ c′ nullable}
\frac{D ⊢ c nullable D ⊢ c′ nullable}{D ⊢ c; c′ nullable}

\frac{D ⊢ c nullable}{⊢ letrec D in c nullable}

Presentation at Microsoft Research, Redmond, June 14, 2004 48

Formal Commercial Contracts cstef@diku.dk

Deterministic Reduction (Backtracking/Deferred Matching)

D, ρ ⊢_{D} Success ⟶^{e} Failure D, ρ ⊢_{D} Failure ⟶^{e} Failure

\frac{ρ ⊧ P [e/X⃗]}{D, ρ ⊢_{D} transmit(X⃗ | P). c ⟶^{e} c[e/X⃗]}  \frac{D, ρ ⊢_{D} c[a⃗/X⃗] ⟶^{e} c′ (f[X⃗] = c) ∈ D}{D, ρ ⊢_{D} f(a⃗) ⟶^{e} c′}
\frac{D, ρ ⊢_{D} c ⟶^{e} d D, ρ ⊢_{D} c′ ⟶^{e} d′}{D, ρ ⊢_{D} c + c′ ⟶^{e} d + d′}  \frac{D, ρ ⊢_{D} c ⟶^{e} d D, ρ ⊢_{D} c′ ⟶^{e} d′}{D, ρ ⊢_{D} c & c′ ⟶^{e} d & d′}
\frac{D, ρ ⊢_{D} c ⟶^{e} d D, ρ ⊢_{D} c′ ⟶^{e} d′}{D, ρ ⊢_{D} c ∥ c′ ⟶^{e} c ∥ d′ + d ∥ c′}  \frac{D ⊢ c nullable D, ρ ⊢_{D} c ⟶^{e} d D, ρ ⊢_{D} c′ ⟶^{e} d′}{D, ρ ⊢_{D} c; c′ ⟶^{e} d; c′ + d′}
\frac{D ⊬ c nullable D, ρ ⊢_{D} c ⟶^{e} d D, ρ ⊢_{D} c′ ⟶^{e} d′}{D, ρ ⊢_{D} c; c′ ⟶^{e} d; c′}  \frac{D, ρ ⊢_{D} c ⟶^{e} c′}{ρ ⊢_{D} letrec D in c ⟶^{e} letrec D in c′}

Formal Commercial Contracts cstef@diku.dk

Nondeterministic Reduction (Eager Matching)

D, ρ ⊢_{N} Success ⟶^{e} Failure D, ρ ⊢_{N} Failure ⟶^{e} Failure

\frac{ρ ⊧ P [e/X⃗]}{D, ρ ⊢_{N} transmit(X⃗ | P). c ⟶^{e} c[e/X⃗]} \frac{(f[X⃗] = c) ∈ D}{D, ρ ⊢_{N} f(a⃗) ⟶^{τ} c[a⃗/X⃗]}

D, ρ ⊢_{N} c + c′ ⟶^{τ} c D, ρ ⊢_{N} c + c′ ⟶^{τ} c′

\frac{D, ρ ⊢_{N} c ⟶^{e} d D, ρ ⊢_{N} c′ ⟶^{e} d′}{D, ρ ⊢_{N} c & c′ ⟶^{e} d & d′}  \frac{D, ρ ⊢_{N} c ⟶^{τ} d}{D, ρ ⊢_{N} c & c′ ⟶^{τ} d & c′}

\frac{D, ρ ⊢_{N} c′ ⟶^{τ} d′}{D, ρ ⊢_{N} c & c′ ⟶^{τ} c & d′} D, ρ ⊢_{N} Success & Success ⟶^{τ} Success

Presentation at Microsoft Research, Redmond, June 14, 2004 50

\frac{D, ρ ⊢_{N} c ⟶^{λ} d}{D, ρ ⊢_{N} c ∥ c′ ⟶^{λ} d ∥ c′}  \frac{D, ρ ⊢_{N} c′ ⟶^{λ} d′}{D, ρ ⊢_{N} c ∥ c′ ⟶^{λ} c ∥ d′}

D, ρ ⊢_{N} Success ∥ c ⟶^{τ} c D, ρ ⊢_{N} c ∥ Success ⟶^{τ} c

\frac{D, ρ ⊢_{N} c ⟶^{λ} d}{D, ρ ⊢_{N} c; c′ ⟶^{λ} d; c′}  D, ρ ⊢_{N} Success; c′ ⟶^{τ} c′  \frac{D, ρ ⊢_{N} c ⟶^{e} c′}{ρ ⊢_{N} letrec D in c ⟶^{e} letrec D in c′}

Presentation at Microsoft Research, Redmond, June 14, 2004 51

Deterministic Reduction (Eager Matching with Explicit Control)

• All nondeterministsm can be reduced to a series of choices and routing decisions!

• We express routing decisions as an element of D = {f, s, l, r}^{∗}.

• A control-annotated event then is an element of D × E.

Formal Commercial Contracts cstef@diku.dk

Deterministic Reduction (Eager Matching with Explicit Choice)

D, ρ ⊢_{C} Success ⟶^{e} Failure D, ρ ⊢_{C} Failure ⟶^{e} Failure

\frac{ρ ⊧ P [e/X⃗]}{D, ρ ⊢_{C} transmit(X⃗ | P). c ⟶^{e} c[e/X⃗]}

\frac{(f[X⃗] = c) ∈ D}{D, ρ ⊢_{C} f(a⃗) ⟶^{τ} c[a⃗/X⃗]} D, ρ ⊢_{C} c + c′ ⟶^{τ} c D, ρ ⊢_{C} c + c′ ⟶^{τ} c′

\frac{D, ρ ⊢_{C} c ⟶^{λ} d D, ρ ⊢_{C} c′ ⟶^{λ} d′}{D, ρ ⊢_{C} c & c′ ⟶^{λ} d & d′}

Presentation at Microsoft Research, Redmond, June 14, 2004 53

\frac{D, ρ ⊢_{C} c ⟶^{λ} d}{D, ρ ⊢_{C} c ∥ c′ ⟶^{e} d ∥ c′}  \frac{D, ρ ⊢_{C} c′ ⟶^{e} d′}{D, ρ ⊢_{C} c ∥ c′ ⟶^{e} c ∥ d′}

\frac{D, ρ ⊢_{C} c ⟶^{λ} d}{D, ρ ⊢_{C} c; c′ ⟶^{λ} d; c′} D, ρ ⊢_{C} Success; c′ ⟶^{τ} c′

\frac{D, ρ ⊢_{C} c ⟶^{e} c′}{ρ ⊢_{C} letrec D in c ⟶^{e} letrec D in c′}

Formal Commercial Contracts cstef@diku.dk

Properties of Reduction Semantics

Proposition 1. Controlled reduction is deterministic: For all c, c′, c′′, E, if c ⟶^{E} c′ and

c ⟶^{E} c′′ then c′ = c′′.

Theorem 2. For all c, e there exists unique c′ such that c ⟶^{e} c′ (with deferred matching) and c/e = C[[c′]].