The Deon Digital Contract Specification Language

Try now

Contract Specification Language

At Deon Digital we are working on a domain-specific language for specifying contracts.

In this blog post we will share details about the contract specification language (CSL henceforth) as well as details on how to get a technology preview version of our implementation. As the technology is being actively developed, expect changes in the future.

In future posts we will share more details about our technology and how to use it, so make sure to check back.

A formal language for contracts

A contract is an agreement between multiple parties stating obligations, permissions, and prohibitions of the parties to perform specific actions.

CSL is a domain specific language for specifying contracts using combinators, where larger contracts are formed by combining smaller contracts using various contract combinators.

A contract written in CSL formally denotes a set of traces of events where each event is in accordance with the conditions of the contract.

Here is a simple example contract:

c = <alice> p:Payment where p.amount = 100
    then
    <bob> d:Delivery where d.item = "Bike"

In the contract c defined above:

First alice must perform a Payment event with an amount = 100, and then
bob must perform a Delivery event with an item = "Bike".

No other sequences of actions would be in compliance with the contract. Using the and combinator, one could change the example contract c into a contract where the order of the Payment and Delivery is not important:

c' = <alice> p:Payment where p.amount = 100
     and
     <bob> d:Delivery where d.item = "Bike"

In the contract c':

alice must perform a Payment event with an amount = 100, and
bob must perform a Delivery event with an item = "Bike".

By saying that c is a contract specification, we mean that a contract is not a program that will perform any of the actions stated in it. Instead, CSL contracts describe only the expected future events.

Having contracts specified in a concise and mathematically precise language is beneficial in terms of communication between people but also allows automation. In particular, contracts can be subject to many kinds of analyses.

A few examples of contract analyses are:

Expected value in terms of resources gained or services rendered by participating in the contract.
Important deadlines in the contract where a choice should be made.
Does a given contract conform to the relevant laws?
Does a given trace of events comply with the obligations and permissions in a contract?

The last example mentioned could also be used in an iterative version, where a computer monitors a contract and incoming events for conformance one at a time.

Getting the technology preview

DISCLAIMER: Before using Deon Digital’s technology read our Terms and Conditions provided in the LICENSE file. It is available on the top right in the web app.

We distribute our technology as a Docker image. The image is available on Docker Hub. Simply do docker run to pull and start the image:

$ docker run -p 8080:8080 deondigital/vitznauerstock
 _____                         _____    _         _              _
(____ \                       (____ \  (_)       (_) _          | |
 _   \ \  ____  ___   ____     _   \ \  _   ____  _ | |_   ____ | |
| |   | |/ _  )/ _ \ |  _ \   | |   | || | / _  || ||  _) / _  || |
| |__/ /( (/ /| |_| || | | |  | |__/ / | |( ( | || || |__( ( | || |
|_____/  \____)\___/ |_| |_|  |_____/  |_| \_|| ||_| \___)\_||_||_|
https://deondigital.com                   (_____|
support@deondigital.com

Welcome to the Deon Digital technology preview image!

This container starts a web service and the necessary backend services
to get the Deon Digital technology stack up and running so you can
play around with it.

Go to http://localhost:8080 and start writing tomorrow's contracts
today!
[...]

After the container starts, the demo web app together with the associated web service should be running.

The web app can be accessed by pointing a browser at http://localhost:8080/. Usage of the web app is described at https://deondigital.com/docs/.

Using the webapp

Using the webapp, one can author contracts, instantiate contract templates, apply events to the running system, as well as query the state in various ways. A web service is also available on port 8080. Going to http://localhost:8080/swagger-ui.html#/ shows the Swagger UI presenting the OpenAPI specification for the web service. To make it a bit easier to interact with the web service, we have created a client library (in TypeScript). The client library is available at GitHub.

If you encounter any problems, please do not hesitate to contact us at support@deondigital.com.

Example specifications

As previously mentioned, the guide can be found at https://deondigital.com/docs/.

As a help for authoring contracts, there is also an extension for Visual Studio Code. The extension provides syntax highlighting, parsing, and type checking of CSL. To install it, search for “deon” in the Visual Studio Marketplace or go to https://marketplace.visualstudio.com/items?itemName=deondigital.csl-support.

Example contract specifications are also available at GitHub.

In the following we develop a contract for the sale of goods from a simple first version to a more complex version.

Step 1: The skeleton of a basic sales contract

The very basic skeleton sales-contract capture only the part that a buyer and seller agree to a contract where first the buyer performs a Payment and only then the seller performs a Delivery.

type Payment: Event {}
type Delivery: Event {}

template Sale(seller, buyer) =
<buyer> Payment then
<seller> Delivery

Step 2: Adding constraints

Naturally, the above is much too simple. We have not specified the payment amounts and the goods to deliver nor any deadlines for the events. We’ll will fix this by extending the definition of the types for Payment and Delivery:

type Payment: Event {
amount: Float
}
type Delivery: Event {
goods: String
}

template Sale(seller, buyer) =
<buyer> p:Payment where
p.amount = 100.0 && p.timestamp <= #2019-03-21#
then
<seller> d:Delivery where
d.goods = "Bike" && d.timestamp <= #2019-03-25#

The Sale-contract now specifies payment of 100.0 and the delivery of "Bike" within set deadlines.

Step 3: Pulling out parameters

We’d like to reuse the Sale-template for more things than handling sales of one particular thing for one particular price so we parameterise the template:

template Sale(seller, buyer, amount, paymentDeadline, goods, deliveryDeadline) =
<buyer> p:Payment where
p.amount = amount && p.timestamp <= paymentDeadline
then
<seller> d:Delivery where
d.goods = goods && d.timestamp <= deliveryDeadline

The number of parameters to the template are a bit high, so we’ll group them in a separate type:

type SaleTerms {
seller: Agent,
amount: Float,
paymentDeadline: DateTime,
buyer: Agent,
goods: String,
deliveryDeadline: DateTime
}

The template is then:

template Sale(terms: SaleTerms) =
<terms.buyer> p:Payment where
p.amount = terms.amount && p.timestamp <= terms.paymentDeadline
then
<terms.seller> d:Delivery where
d.goods = terms.goods && d.timestamp <= terms.deliveryDeadline

Step 4: Refining the Payment-step of the contract

In the latest iteration of the sales contract, fulfillment of the payment is represented by a single event Payment where the amount stated is exactly 100.0. A conseqence is that an event that specifies an amount only slightly different than 100.0 or slightly delayed will not be considered a valid fulfillment of the payment. We will change the Sale-template so that the payment is a separate sub-contract that will also be called Payment. The separation of payment into a subcontract allow us to have a more refined notion of the payment fulfillment. First the new Sale-template where we’ve simply copied the old version of the payment into a separate template:

template Payment(terms) =
<terms.buyer> p:Payment where
p.amount = terms.amount && p.timestamp <= terms.paymentDeadline

template Sale(terms: SaleTerms) =
Payment(terms)then
<terms.seller> d:Delivery where
d.goods = terms.goods && d.timestamp <= terms.deliveryDeadline

The first refinement we’ll make is to allow late payment but which then incurs a fixed fee:

template Payment(terms) =
<terms.buyer> p:Payment where
p.amount = terms.amount && p.timestamp <= terms.paymentDeadline
or
<terms.buyer> late:Payment where
late.timestamp > terms.paymentDeadline &&
late.amount = terms.amount + 50.0

In the Payment-template above, a Payment–event can be performed before the agreed deadline OR it can be performed after the deadline provided the amount specified in the event is 50.0 higher than initially agreed.

Step 5: refining the delivery

In a similar fashion to how we refined the payment in a subcontract, we can do the same for the delivery. The initial simple version is:

template Delivery(terms) =
<terms.seller> d:Delivery where
d.goods = terms.goods && d.timestamp <= terms.deliveryDeadline

template Sale(terms: SaleTerms) =
Payment(terms)
then
Delivery(terms)

For the sake of the example, the delivery template will be changed so that either

the seller must ensure the delivery before the deadline, or
if the seller has not delivered before the deadline, the buyer has the right to cancel the purchase. The seller is then obliged within 5 days to pay back the amount originally payed:

template Delivery(terms) =
<terms.seller> d:Delivery where
d.timestamp <= terms.deliveryDeadline && d.goods = terms.goods
or
( <terms.buyer> c:Cancel where
c.timestamp > terms.deliveryDeadline
then
<terms.seller> b:Payment where
b.amount = terms.amount &&
b.timestamp <= DateTime::addDays c.timestamp 5
)

Step 6: flexible completion

The sales template is now:

template Sale(terms: SaleTerms) =
Payment(terms) then
Delivery(terms)

As specified above, it’s required that the payment subcontract is completed before allowing delivery to take place. We can relax this constraint by using the and combinator instead of then to obtain a contract where the order in which to complete the subcontracts does not matter:

template Sale(terms: SaleTerms) =
Payment(terms) and
Delivery(terms)

In the version using and the seller is allowed to complete the delivery before receiving payment, but the buyer is obliged to fulfill the Payment-contract in any case.

The final sales contract

The final specification is given below.

type Payment: Event {
amount: Float
}
type Delivery: Event {
goods: String
}

type SaleTerms {
seller: Agent,
amount: Float,
paymentDeadline: DateTime,
buyer: Agent,
goods: String,
deliveryDeadline: DateTime
}

type Cancel: Event{}

template Sale(terms: SaleTerms) =
Payment(terms)
and
Delivery(terms)

template Main(seller, buyer) =
Sale(SaleTerms {
seller = seller,
buyer = buyer,
amount = 100.0,
paymentDeadline = #2019-03-22#,
goods = "Bike",
deliveryDeadline = #2019-03-25#
})

In the above, a Main-template has been added to make it easy to instantiate the Sale-template from the webapp included in the docker image.

References

CSL is based on research done at the University of Copenhagen over several years by several people. A brief list of papers that describe prior work is given below.

Contract Formalisation and Modular Implementation of Domain-Specific Languages (Ph.D. Dissertation, pdf)
POETS: Process-oriented event-driven transaction systems (doi)
Compositional specification of commercial contracts (doi)
Composing contracts: an adventure in financial engineering (link)
How to write a financial contract (pdf)