Contracts 101

In a nutshell, a CSL contract is a specification of a set of sequences of events. Each such event sequence is a complete way to conclude the contract successfully. Events are represented by event values which are inserted into the runtime system in a platform-dependent way. In the following, we shall use the terms “event” and “event value” interchangeably except where noted otherwise.

Execution of CSL contracts can be monitored as they unfold in time under the arrival of events. Specifically, given an event, a contract can be reduced to a contract that represents the remaining obligations after the event has occurred.

Contracts are expressed using composition: Smaller contracts are combined into larger ones. A larger contract specifies a behaviour that is a combination of its constituent smaller contracts. The smallest contracts do not do anything other than being “finished” – either signaling a success or failure (“contract breach”) state. New events are described by using a prefix combinator, which uses a predicate on incoming events to decide whether it is allowed or not. Many other contract combinators exist; for a comprehensive list see the contract reference.