Contract language reference¶
This section presents an overview of the CSL language constructions for the composition of contracts.
The atomic contracts of CSL are the smallest building blocks:
The non-atomic contracts all specify behaviour relative to smaller sub-contracts. Herein lies the composability of CSL: We formulate general structures that we may re-use across several contracts. There are five ways to compose contracts:
- expecting the occurrence of an event before another contract;
- putting two contracts in sequence;
- composing two contracts concurrently;
- making a choice between two contracts; and
- wrapping contracts in templates and recursive templates.
Note that the code examples in the following sections will sometimes consist of snippets of CSL code, not entire CSL specifications that can be copy-pasted and run. We have attempted to add comments in the code snippets to make it clear which parts have been left out, so it should not be too much work to copy and reuse the example snippets.
The successfully completed contract¶
A successfully completed contract is written as:
success
Because it is completed, this contract accepts no events.
The breached contract¶
The failed, or breached, contract is written as:
failure
A breached contract is in a state of failure and therefore it accepts no events.
The prefixed-contract¶
A “prefix-contract” is a contract that expects an event satisfying some predicate and after receiving a matching event it becomes a new contract. The general format is:
<AGENT> x:EVENTTYPE where PREDICATE
The above general form should be read as:
The agent identified by the valueAGENT
must issue an event of the typeEVENTTYPE
. This event is calledx
, and the predicatePREDICATE
must evaluate toTrue
. If it does, consume the event and evolve tosuccess
. Otherwise, do nothing.
If the originator of the event is unimportant, we may write *
, matching any agent.
Likewise, we may completely omit the where-clause with the predicate.
Doing so corresponds to matching any event with the given type.
Examples¶
The following example illustrates how one could match certain Foo
events from Alice
:
<alice> n: Foo where n.timestamp < #2017-08-31T23:00:00Z#
This is a specification of a contract that expects an event of type Foo
from Alice
where the timestamp
field is before August 31st at eleven o’clock in the evening.
After receipt of such an event, the reduced contract is success
.
If we instead wanted to match just any event of type Foo
, with no constraints on either the fields of the event or on the originating agent, we could write the following:
<*> Foo
This snippet is equivalent to writing
<*> Foo where True
which is again equivalent to
<*> f: Foo where True
We may chain together several prefix contracts using the then
sequence combinator.
For example, the following contract snippet specifies that first a payment event from Alice
and then a delivery event from Bob
must occur, after which no more events may occur:
type Payment : Event { receiver: Agent, amount: Int }
type Delivery : Event { receiver: Agent }
// ... definition of Payment and Delivery events ...
template C1(alice,bob) =
<alice> p: Payment where
p.receiver = bob &&
p.timestamp = #2017-08-24T12:00:00Z#
then
<bob> d: Delivery where
d.receiver = alice &&
d.timestamp < #2017-08-26T12:00:00Z#
Now, assume that the agent Alice
has input the following event:
Payment {
agent = alice,
timestamp = #2017-08-24T12:00:00Z#,
receiver = bob
}
This event satisfies the first predicate, so our contract accepts it and evolves into its residual:
template C2(alice,bob) =
<bob> d: Delivery where
d.receiver = alice &&
d.timestamp < #2017-08-26T12:00:00Z#
Bob
now issues an event:
Delivery {
agent = bob
timestamp = #2017-08-25T12:00:00Z#,
receiver = alice
}
The second predicate of the original contract (or the first predicate of the residual contract) is satisfied with this event, so the contract evolves into:
template C3() = success
No more events may be applied; the sequence of events that our contract specified was observed.
Sequentially composed contracts¶
Given two contracts c1
and c2
, their sequential composition is the contract:
c1 then c2
A contract that is a sequential composition of two other contracts specifies that the left-hand contract must be completed before the events of the right-hand contract can be considered.
Precedence of binary operators¶
The precedence of the three binary contract operators is as follows:
then
binds tighter thanand
, which binds tighter thanor
.
This means that the following
a then b or c and d then e
is equivalent to
(a then b) or (c and (d then e))
When you write a contract and need a different structure than the default imposed by the operators’ precedence levels you can use parentheses to change it.
Examples¶
Consider the following example where we define the two contracts AlicePays
and BobDelivers
:
template AlicePays(alice,bob) =
<alice> p: Payment where p.receiver = bob
template BobDelivers(alice,bob) =
<bob> d: Delivery where d.receiver = alice
Given these definitions, the following two contracts are equivalent:
// Combine two smaller contracts into one.
template AlicePaysThenBobDelivers(alice,bob) =
AlicePays(alice,bob) then BobDelivers(alice,bob)
// Equivalent formulation:
template AlicePaysThenBobDelivers2(alice,bob) =
<alice> p: Payment where p.receiver = bob
then
<bob> d: Delivery where d.receiver = alice
Concurrently composed contracts¶
The concurrent composition of two contracts c1
and c2
is the contract:
c1 and c2
Composing contracts concurrently yields a contract that accepts all event sequences that are accepted by either the two constituent contracts, where the sequences might be interleaved.
For any contract c
, the contracts success and c
and c and success
are equivalent.
The precedence level is below then
and above or
.
Examples¶
Say we wanted to express a sales contract where the buyer was free to pay the seller before or after delivery of the goods.
The following contract is a reformulation of our sales contract between Alice
and Bob
that allows for just that:
template SaleWithoutTemporalRestrictions(alice,bob) =
<alice> p: Payment where p.receiver = bob
and
<bob> d: Delivery where d.receiver = alice
This contract specifies that Alice
and Bob
must issue Payment
and Delivery
events, but not that they must occur in any specific order.
Both the event sequence “Payment
-then-Delivery
” and “Delivery
-then-Payment
” are valid according to this contract.
After applying the event
Payment {
agent = alice,
timestamp = #2017-08-24T13:37:00Z#
receiver = bob
}
the residual contract will be
success
and
<bob> d: Delivery where d.receiver = alice
This contract accepts just the Delivery
event from Bob
.
If we had instead applied a Delivery
event first, the residual contract would have been
<alice> p: Payment where p.receiver = bob
and
success
Now the contract expects a Payment
event from Alice
next.
Choice between contracts¶
The choice between two contracts c1
and c2
is the contract:
c1 or c2
The choice-contract allows composition of two independent contracts into a new contract that expects exactly one of the two contracts to be completed. Depending on the shape of the two sub-contracts and the incoming event, one or the other will be picked as the residual contract.
The precedence level is below both then
and and
.
Examples¶
Consider a scenario in which we would like Alice
to pay a sum of money and the sum depends on whether she pays before or after Christmas eve 2018.
Each of the sub-scenarios can be modelled with a simple prefix-contract, and we can use or
to combine them in the appropriate way:
val deadline0 = #2018-12-24T13:37:00Z#
template PayBeforeOrAfterChristmas0(alice) =
<alice> p: Payment where p.timestamp <= deadline0
or
<alice> p: Payment where p.timestamp > deadline0
The contract can evolve in two different ways.
Either Alice
performs a Payment
before the deadline of 2018-12-24T13:37:00
with an amount of 100
, or Alice
performs a Payment
after the deadline and then the amount has to be 200
.
Exactly one of these two things has to occur in order for the entire contract to be satisfied.
Applying a Payment
event either before or after the deadline yields the residual contract
success
This is because the residual contract of the two individual prefix-contracts are both success
.
Consider instead the following variation on the contract, where either Santa Claus
or Bob
sends a Delivery
event depending on whether the Payment
came before or after Christmas:
val deadline1 = #2018-12-24T13:37:00Z#
template PayBeforeOrAfterChristmas1(alice,bob,santaClaus) =
<alice> p: Payment where p.timestamp <= deadline1
then
<santaClaus> Delivery
or
<alice> p: Payment where p.timestamp > deadline1
then
<bob> Delivery
Applying a Payment
event before the deadline will now yield the residual contract
<santaClaus> Delivery
If the Payment
came after the deadline, the residual would instead be
<bob> Delivery
The success
contract denotes a contract that is considered to have been completed in a successful manner.
If we combine that with some other contract c
using or
, we construct a contract where the events of c
are permitted but not obligated.
Suppose we construct a contract as follows:
template C(alice) = <alice> Payment or success
This is a contract where Alice
may perform a Payment
event if she chooses.
We can extend the permission contract to a contract where there is an optional choice to be made:
type Option1 : Event {}
type Option2 : Event {}
type Action : Event {}
template OptionalChoice(alice,bob,charlie) =
<alice> Option1
then
<bob> Action
or
<alice> Option2
then
<charlie> Action then success
In this contract, Alice
may choose to perform either of the events Option1
or Option2
, resulting in either the residual contract where Bob
can perform an Action
or the contract where Charlie
can perform an Action
.
She may also choose not to send any events; the final composition with the success
contract allows that.
Contract templates¶
A contract template with the name TemplateName
has the general form:
template [c0, ..., cn] TemplateName (p0, ..., pm) = BODY
where c0
, …, cn
are contract parameters and p0
, …, pm
are value parameters.
In the special case where there are zero contract parameters, we may also use the equivalent shorthand:
template TemplateName (p0, ..., pm) = BODY
A contract template, either with or without contract parameters, is a name for a contract that can be re-used. Using a contract template means instantiating the contract and value parameters, if any, with contract arguments and value arguments, respectively. This means that we can capture general contract design patterns with contract templates and apply them whenever they are needed.
CSL allows the use of local contract templates: Templates that are only usable inside some other contract. This can be handy if we need some contract template that is too specific to be at the top-level but where we would still like the benefits from encapsulating a pattern. The syntax for a local contract template is:
// ... inside some contract definition
let template [c0, ..., cn] TemplateName (p0, ..., pm) = TEMPLATEBODY
in
BODY
Inside of the contract body BODY
we may now use the template TemplateName
, but it is not visible from the outside nor is it visible inside TEMPLATEBODY
.
Earlier definitions are visible in later ones but not vice versa.
Examples¶
In its most basic form we can write
template JustSucceed() = success
which effectively serves as an alias for the success
contract.
This contract template takes no value parameters.
Say we want to express that a Payment
event from Alice
for some not-yet-specified amount of money has to occur.
There is just one (value) parameter to this contract template, namely the sum of money.
We express it as follows:
// ... Payment event defined here
template AlicePaysAmount(amount,alice) =
<alice> p: Payment where p.amount = amount
If now want to express some sale where Alice
pays 42 euros and then, for the sake of simplicity, nothing more happens, we write
template SomeSale(alice) = AlicePaysAmount(42,alice)
Note that this is itself a contract template (still with zero contract parameters). In the section about instantiating contracts it is explained how to get from “static” descriptions of contracts to something that actually lives and runs somewhere.
We might often need to express that some contract be dependent on a signature from an agent. This is a quite general pattern, so we formulate it as a contract template:
type Signature : Event {
// ... Signature event defined here with appropriate fields
}
template [c] SignAndContinue(agent) =
<agent> Signature then c
This contract template takes one contract parameter, c
, and one value parameter, agent
, and it constructs a prefix-contract requiring a Signature
event from agent
before it evolves into the contract c
.
We might want to refine this pattern by allowing some default contract to happen if the agent can’t issue a Signature
.
Our contract template just needs two contract parameters instead of one to achieve this:
// ... Signature event defined as above
template [cSigned, cUnsigned] SignOrDefault(agent) =
(<agent> Signature then cSigned) or cUnsigned
Here we use the or
combinator to choose between the contract where the agent signs which continues as cSigned
, and the contract called cUnsigned
where the agent does not sign.
It could of course be generalized to handle different kinds of signatures, default cases, etc.
Templates themselves can be nested using the let ... in
construct:
type SayHello : Event {}
type SayGoodbye : Event {}
template HelloHelloGoodbyeLocal(agent) =
let
// 'agent' says "hello" and the template evolves
// into the contract given by 't'
template [t] Hello() = <agent> SayHello then t
// 'agent' says either "goodbye" and the contract
// evolves into 't', or she says "hello" and the
// contract evolves into 't'.
template [t] Goodbye() =
(<agent> SayGoodbye then t) or Hello[t]()
in
// 'agent' says "hello" twice before saying
// either "goodbye" or "hello" once and then
// the contract ends successfully.
Hello[Hello[Goodbye[success]()]()]()
In this example we exploit the fact that the template Goodbye
can use the template Hello
.
We could write the above without the use of local templates as follows:
// ... SayHello and SayGoodbye defined here ...
template HelloHelloGoodbye(agent) =
<agent> SayHello then
<agent> SayHello then
(
<agent> SayGoodbye
or
<agent> SayHello
)
Recursive contract templates¶
A recursive contract template with the name TemplateName
has the form
template rec TemplateName(p0, p1, ..., pm) = TEMPLATEBODY
where p0
, …, pm
are value parameters.
Unlike non-recursive contract templates, recursive contract templates are not allowed to have any contract parameters.
Recursive contract templates work like normal contract templates, except that TEMPLATEBODY
may call itself by calling TemplateName
.
All recursive calls must be guarded, which means that at least one event must be accepted by TEMPLATEBODY
before a call to TemplateName
has to be unfolded to determine what the possible next events of the residual contract is.
If multiple recursive contract templates will need to call each other, the following general form can be used:
template rec TemplateName-0( ... ) = TEMPLATEBODY-0
with TemplateName-1( ... ) = TEMPLATEBODY-1
with ...
with TemplateName-n( ... ) = TEMPLATEBODY-n
All template names TemplateName-0
, …, TemplateName-n
can be used recursively in all bodies TEMPLATEBODY-0
… TEMPLATEBODY-n
.
The same restrictions regarding guardedness apply.
Recursive contract template examples¶
Consider the following recursive contract template PingPong
:
type Ping : Event {}
type Pong : Event {}
template rec PingPong() =
<*> ping:Ping then <ping.agent> Pong then PingPong()
or
success
Instantiating this template yields a contract which accepts the event Ping
from any agent and then requires the same agent to generate an event Pong
, after which it goes back to accepting another Ping
event from another agent by calling PingPong()
.
The contract can be terminated as long as all Ping
events have been matched by a corresponding Pong
.
For example, if Alice
applies Ping
to PingPong()
, then the residual contract is
<alice> Pong then PingPong()
The following example uses mutual recursion to model a house where a specified agent can move inside and outside and, depending on where the agent is, may perform tasks such as watching TV or mowing the lawn.
type WatchTv : Event {}
type GoOutside : Event {}
type GoInside : Event {}
type MowLawn : Event {}
template House(agent) =
let template rec Inside() =
<agent> WatchTv then Inside()
or <agent> GoOutside then Outside()
with Outside() =
<agent> MowLawn then Outside()
or <agent> GoInside then Inside()
or success
in
Outside()
We have defined the mutually recursive templates as local templates inside a non-recursive contract template to ensure that a House
contract can only be instantiated starting in the Outside
state.
In each of the states Inside
and Outside
, the agent may perform any number of WatchTv
and MowLawn
events, respectively, but the agent can only go outside if already inside, and vice versa.
Note that the contract may only successfully terminate when the agent is outside.
Guardedness¶
One has to take care that a (mutually) recursive contract template definition is well-guarded, as unguarded contracts do not have a well-defined semantics. The CSL system will automatically check if a contract is well-guarded and reject it with a descriptive error message otherwise.
A recursive template definition is unguarded whenever it is possible for it to call itself without first consuming an event. For example, the following recursive template does nothing but call itself, and so is clearly unguarded:
template rec Unguarded() = Unguarded()
Unguarded recursive templates are problematic because they can be used to express contracts which has to be unfolded indefinitely before we can determine whether a given event can be applied or not. For example, consider the following unguarded contract template:
type Count : Event { n: Int }
template rec Unguarded(n) =
<*> p:Count where p.n = n or Unguarded(n+1)
The instantiation Unguarded(0)
can, without applying any events, be unfolded to any of the following:
<*> p:Count where p.n = 0 or Unguarded(1)
<*> p:Count where p.n = 0 or p:Count where p.n = 1 or Unguarded(2)
<*> p:Count where p.n = 0 or p:Count where p.n = 1 or
p:Count where p.n = 2 or Unguarded(3)
...
and so on.
In this case, if we are given the event Count { n = 42 }
, then the system will have to figure out that it needs to do 42 unfoldings before it reveals a prefix matching the event.
Given the event Count { n = -42 }
, the system has to analyze the contract to determine that no number of unfoldings can reveal a matching prefix.
In general, an unguarded unfolding can generate much more complicated mathematical sequences, and it can be shown that it is theoretically impossible to determine, in general, if there exists a number of unfoldings that reveals a matching prefix or not.
The above example becomes guarded if we change or
to then
(and add success
to allow the contract to terminate):
template rec Guarded(n) =
<*> p:Count where p.n = 1 then Guarded(n + 1)
or success
While we can still unfold the recursive calls indefinitely, we do not have to do that in order to determine whether a given event can be accepted: any event must be matched by the prefix that is visible now, so unfolding Guarded(n+1)
will not reveal any new information.
It is generally easy to spot unguarded contracts simply by checking that all recursive calls occur below a prefix. However, there is one common pitfall that may lead to accidental unguardedness. Consider the following example:
template Nullable() = <*> Count or success
template rec Unguarded() = Nullable() then Unguarded()
The call to Unguarded()
is apparently below a then
, making it appear guarded on cursory inspection.
However, since it is possible to terminate Nullable()
via the right alternative without consuming any events, the call to Unguarded()
is exposed.
Contract abbreviations¶
A contract abbreviation with the name abbreviationName
has the general form:
contract abbreviationName = ABBREVIATIONBODY
This defines an abbreviation for the contract ABBREVIATIONBODY
and binds it to a contract variable with the name abbreviationName
.
Abbreviations are defined using the contract
keyword with a lowercase name.
They are distinguished from templates in that it is not possible to specify any contract or value parameters, and furthermore contract abbreviations cannot refer to themselves, which for the above example means that abbreviationName
may not occur as a contract variable within ABBREVIATIONBODY
.
CSL allows the definition of local abbreviations that are only visible within contracts. The syntax for a local contract abbreviation is
// ... inside some contract definition
let
contract abbreviationName1 = ABBREVIATIONBODY1
contract abbreviationName2 = ABBREVIATIONBODY2
...
contract abbreviationNameN = ABBREVIATIONBODYN
in
BODY
Inside BODY
we may use abbreviationName1
, abbreviationName2
, …, abbreviationNameN
as a contract variables, but they are not visible from the outside.
Furthermore, each ABBREVIATIONBODYi
may use the previously defined abbreviations abbreviationName1, abbreviationName2, ..., abbreviationName(i-1)
.
Abbreviations can be used to reformat a complex contract to make it more readable, but otherwise they add no expressive power to the language. It is generally preferable to use abbreviations when the full power of contract templates are not needed, since this communicates to the system that the abbreviations are intended to be used as such, and that any self-reference is accidental and should be flagged as an error.
Examples¶
In the following example, we express a contract where some agent may either borrow a car or buy it, after which the agent is allowed to drive it. If the car was only borrowed and not bought, then it must be returned again when the agent has finished driving it. To avoid repeating the specification of what it means to drive a car, we define that part of the contract using an abbreviation:
type BorrowCar : Event {}
type ReturnCar : Event {}
type BuyCar : Event {}
type DriveCar : Event {}
type TurnOnCar : Event {}
type TurnOffCar : Event{}
template Drive(agent) =
let
contract driveCar =
<agent> TurnOnCar then
<agent> DriveCar then
<agent> TurnOffCar
in
(<agent> BorrowCar then
driveCar then
<agent> ReturnCar
)
or
(<agent> BuyCar then
driveCar
)
We could also have defined a local template DriveCar()
instead, but that would have been unnecessary since the driveCar
contract never needs to call itself.
In this way, readers of our contract can determine just by looking at the definition head of driveCar
that it is truly just an abbreviation, and that its body cannot refer back to itself.