Temporal Higher-Order Contracts
Tim Disney

Cormac Flanagan

Jay McCarthy

University of California, Santa Cruz

University of California, Santa Cruz

Brigham Young University

Abstract
Behavioral contracts are embraced by software engineers because
they document module interfaces, detect interface violations, andhelp identify faulty modules (packages, classes, functions, etc).
This paper extends prior higher-order contract systems to also express and enforce temporal properties, which are common in software systems with imperative state, but which are mostly left implicit or are at best informally specified. The paper presents botha programmatic contract API as well as a temporal contract language, and reports on experience and performance results from implementing these contracts in Racket.
Our development formalizes module behavior as a trace of
events such as function calls and returns. Our contract system provides both non-interference (where contracts cannot influence correct executions) and also a notion of completeness (where contracts
can enforce any decidable, prefix-closed predicate on event traces).
Categories and Subject Descriptors D.3.1 [Formal Definitions
and Theory]: Semantics; D.3.3 [Language Constructs and Features]: Constraints
General Terms Languages, Reliability, Security, Verification.
Keywords Higher-order Programming, Temporal Contracts

1.

Contract Expressiveness

Large software systems typically consist of many modules (e.g.,
packages, classes, functions) produced by different development
teams. When the system fails, an initial difficulty is fault localization: identifying the module that failed to perform as expected. Undocumented module interfaces are problematic for various reasons,not least because they lead to disagreements about which module
is considered “at fault” and should be fixed.
Software engineers embrace behavioral contracts because they
address many of these problems. In particular, behavioral contracts provide a mechanism to explicitly document each module’s assumptions and guarantees; to dynamically detect contract
violations; and to identify faulty modules. Behavioral contracts
are widely used in procedural, object-oriented, and functional
languages, including Eiffel [36], C [42], C# [32], Haskell [26],Java [28], Python [44], Scheme [19, 15, 22], and Smalltalk [10].
Existing contract systems can express a range of interface specifications. Below, we consider a range of possible specifications for

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
ICFP’11, September 19–21, 2011, Tokyo, Japan.
Copyright c 2011 ACM 978-1-4503-0865-6/11/09. . . $5.00

a sort routine, not all of which are supported by existing contractsystems.
1. The sort function takes two arguments, an array of positive
integers and a comparison function cmp.
This standard, first-order precondition constrains how sortshould be called, that is, what arguments are valid. These kindsof basic first-order contracts are supported by most contractsystems, for example, Eiffel [36].
2. The argument function cmp in turn requires two arguments, both
positive integers.
This higher-order precondition constrains how the sort module
can call the function argument cmp, and so is a guarantee provided by sort rather than an obligation on the client. Higherorder contract systems [19, 15, 22, 24, 45] support such preconditions by wrapping the cmp argument to enforce this property
dynamically.
3. The sort function is not re-entrant–it can only be called after
all previous sort invocations have completed.
Unlike the previous contracts that constrain how functions may
be called, this temporal contract constrains when sort can becalled [12, 13]. This constraint implies that sort must be usedcarefully in a multithreaded setting. Moreover, it also imposes
restrictions in a sequential setting, since for example, cmp is
not allowed to call sort. A variety of prior systems support
such first-order temporal contracts: for example, MOP [33],Tracematches [39], PathExplorer [25], Eagle [6], RuleR [7],and others.
4. sort is granted a capability to call the cmp function only until
sort returns.
This last contract is a higher-order temporal contract in that it
combines both higher-order and temporal aspects. It expresses
a temporal constraint, not on sort itself, but on its higher-orderinteraction with the cmp argument it was passed.
To enforce this contract, it is not sufficient to instrument all
cmp functions passed to sort, since these may legally be calledfrom other call sites after sort returns. It is also insufficient
to instrument only calls to cmp within sort, since sort mightpass a reference to cmp to a third party, who in turn could call
cmp after sort returns.
Our study of a widely-used standard library (see Section 8) indicates that higher-order temporal constraints are common in software systems with imperative state, but are mostly left implicit or
are at best informally specified. In this paper, we study how to express and enforce such higher-order temporal contracts. Our development leverages and combines techniques from prior higher-ordercontract systems [19, 15, 22] and from first-order temporal contractsystems [33, 39, 25, 6, 7]. We also address blame assignment in a
temporal setting. For the example considered above where sort

passes cmp to a third party that later calls cmp, our temporal contract system immediately detects the error, halts execution, and correctly blames the sort module, even though it is neither the caller(the third party) nor the callee (cmp) of the erroneous function call.
In a very general sense, contracts provide a means to specify
and restrict the behavior of a module. In a higher-order imperative
setting, this notion of a module’s behavior is quite complex, as it
can involve higher-order callbacks, mutual recursion, and sharingof imperative state between modules. Understanding the temporaland higher-order aspects of module behavior is a prerequisite todeveloping expressive contracts for constraining this behavior.
The first step in our investigation is to formalize the behaviorof each module as a sequence of events, namely remote procedure
calls to other modules and matching returns, etc. We start with
an operational abstract machine that extends a control-store machine [16, 17] with a remote procedure call mechanism. This abstract machine then generates structural and scoping constraints on
event sequences, and so “bootstraps” the game semantics. Module
linking involves running abstract machines in parallel and appropriately routing events between them.
In this setting, the observable behavior of a module is captured by the set of possible event sequences it can generate. Consequently, the most general notion of a contract is a predicate describing permitted event sequences (that is, permitted observablebehaviors of the module). We require that the set of event sequences
permitted by a contract is prefix-closed, so that errors are detected
as soon as they occur. We also require that contracts are computablepredicates.
Based on this formalism, we provide a monitor interface
whereby programmers can express arbitrary contracts as predicatesover event sequences. This monitor interface provides:
1. non-interference, since the monitor code does not gain references (a.k.a. capabilities [37]) to mutable data or to functions,and so the monitor cannot perturb correct program executions,but can only halt erroneous executions;1 and2. a notion of completeness that we call trace completeness, meaning that a monitor can impose any computable prefix-closed
predicate on a module’s event trace (i.e., on its observable behavior).
It is straightforward to achieve one of non-interference or tracecompleteness; achieving both simultaneously requires a more subtle design since we need to provide monitors with all information
about the observed trace (to achieve trace completeness) without
giving it access to function references or to mutable state (in orderto ensure non-interference).
In addition to this programmatic monitor interface, we also provide a declarative contract language for expressing both structuraland temporal specifications of a module’s behavior. The structural
specifications expresses constraints on function arguments and results, and also names each function (including function arguments
such as cmp above). The temporal specifications is a regular grammar2 over calls and returns of functions named in the structuralcomponent, and includes dependent sequences to express, for example, that a call to release(x) must be preceded by a call toacquire(x), for any resource x. Each constraint in this language
is compiled into a monitor, and thus leverages the monitor interface
to provide non-interference and blame assignment.

Contributions The main contributions of this paper are:
• We formalize the behavior of imperative higher-order modules

as event sequences, using an operational semantics (section 3).
• We formalize a contract as a computable, prefix-closed predi-

cate on event sequences (section 4).
• We present a monitor interface that satisfies the twin design

goals of non-interference and trace completeness (section 5).
• We show how to track and assign blame for complex temporalcontracts (section 6).
• We present a declarative contract language for expressing

mixed structural and temporal contracts (section 7).
• We describe a Racket [22]3 implementation of both the monitor

interface and the contract language, and include preliminary
performance and usability results (section 8).4

2.

Motivating Examples

We first illustrate how our proposed contract language succinctly
captures important structural and temporal constraints of softwareinterfaces.
To start, the following formal contract captures all four of thedesired constraints for sort informally outlined above:
SortContract =sort : (List Pos)
(cmp : Pos → Pos → Bool)→ (List Pos)
where not ... call(sort,_) !ret(sort,_)*call(sort,_)and not ... ret(sort,_) ... call(cmp,_)

// 1
// 2

// 3
// 4

By convention, we use Initial Capitals to denote contract names
such as Bool and Pos (for positive numbers) and SortContract.
The notation “name : Dom → Rng” describes a function contract
where the argument and result values should satisfy contracts Domand Rng respectively. The optional “name :” prefix associatesa name with each function, which can then be referenced in thewhere clause. This clause expresses a regular constraint over thesequence of events (calls and returns of these named functions).
The pattern “...” matches any sequence of events, and the notoperator has low precedence, so its argument extends to the end of
the where clause. The pattern “ ” matches any argument in a callor any return value in a ret. The prefix “!” denotes the negationof a single event (unlike “not”, which negates a pattern), and thepostfix “*” denotes a sequence matching the preceding pattern.
Thus, “!ret(sort, )*” denotes any sequence of events that does
not include a return from sort. Whereas, “not ret(sort, )*”matches any traces that are not only returns from sort, such as
traces that start with a return from sort, a call to something else,then any other events.
Constraint (3) declares sort to be non-reentrant; it cannot becalled a second time before the first call returns. Constraint (4) isa little more complex in that it is a higher-order temporal contract.
Each call of sort introduces a binding for cmp in the above contract, and so cmp denotes not just one function, but any comparison
function ever passed to sort. Each such comparison function has
an associated sort invocation, and constraint (4) explicates thatthe comparison function cannot be called after the associated sort
invocation returns.

1 Earlier work on higher-order contracts [20] also proposed non-interference

as a design goal, but did not achieve a notion of completeness.
2 We focus on checking safety but not liveness properties, and so do notneed the additional expressiveness of temporal logics such as LTL [40].

3 Formerly known as PLT Scheme.
4 The implementation is available in the core Racket distribution as of July

2011 in the “unstable” collection.

As a simpler example, an implicit property of many libraryfunctions is that they are expected to return immediately after being
called, with no intervening callbacks to client code. We document
this atomicity property with the following contract, which detects
an error if a call to f is not immediately followed by a matching
return.
AtomicContract =f : Any → Any
where not ... call(f,_) !ret(f,_)
Since internal calls within f are not externally visible, this contract
still permits arbitrary internal computation, but forbids callbacks tooutside code. Note that this atomicity guarantee is useful even in asequential setting.
The following interface describes a file system whose open
method returns a File object corresponding to the given file name.
Each File object contains methods for reading, writing, and closing that file, with the temporal constraint that once the file is closed
these methods should not be called. Note that this temporal constraint is scoped to its enclosing File object: calling close on one
file does not influence the ability to access other open files. Put
differently, the alphabet of close events is unbounded.
FileSystemContract =open : String → FileContract
FileContract =Record read : Unit → String
write : String → Unit
close : Unit → Unit
where not... ret(close,_) ...
(call(close,_) | call(read,_) | call(write,_))Finally, consider the following contract that documents a standard alloc/free interface on some resource, where each resource
instance has an associated integer handle z. After a resource handlez has been freed, it should not be freed again until after it has been
re-allocated. The pattern “?z” binds a variable z to an argument/result, allowing z to be referenced later in the grammar.
AllocFreeContract =Record alloc : Unit → Int
free : Int → Unit
where not... call(free,?z) !ret(alloc,z)* call(free,z)
We now proceed to investigate a contract system that can express
these kinds of mixed structural and temporal constraints.

3.

A Model of Module Interactions

The starting point for our investigation of contract expressiveness is
an imperative higher-order language, namely the untyped imperative lambda calculus with constants (c) and mutable reference cells.
e::=x | λx. e | e e | c | ref e

To simplify our presentation, we use standard lambda-calculus encodings of let expressions, sequencing, n-ary function definitions
and calls, pairs (with accessors fst and snd), n-ary records, sums,
booleans, conditionals, recursive definitions, and assertions. Thus,
despite its simplicity, this language is sufficient to model many aspects of modern languages, including encapsulated behavior (via
λ-expressions) and both encapsulated and shared imperative state(via ref).5
5 The language does not support concurrency, whose interaction with tem-poral higher-order contracts remains an important topic for future work.

To facilitate our technical development, we take an “interfaceoriented” view to reference cells, as proposed by Reynolds [41],whereby ref e returns a pair of getter and setter functions for reading and updating the newly created reference cell. This representation allows calls to getter/setter functions to also model operations
on shared mutable data, and so all inter-module interaction is modeled by function calls and returns.
A module generally denotes a syntactic construct such as a
package, class, function, etc. In the setting of the λ-calculus, wetake a module to simply mean a closed expression e. Two modules
e1 and e2 can be linked via function application (e1 e2 ).
As an example, consider the following module twice with anassociated test harness H:
twice
H

def

=
def
=

(λf. λx. f (f x))(λt. t (λx. x+1) 4)

The linked program (H twice) passes the result of twice into H,
which then calls twice with appropriate arguments (λx. x+1) and4. The module twice in turn calls back into the (λx. x+1) function
provided by H. Thus, despite its simplicity, the imperative lambda
calculus permits rich patterns of module interaction and callbacks.
The goal of this paper is to formalize (and subsequently constrain,
via contracts) these interactions.
3.1

Semantics of Modules

We formalize the semantics of a module using the operational abstract machine called the CSI machine defined in Figure 1. Thismachine includes both code (C) and a store (S), and so in part functions much like Felleisen’s hC, Si machine [16, 17]. The [CALL]
rule performs standard β-reduction within an evaluation context E.
The rule [PRIM] leverages an auxiliary δ function to define the semantics of primitives. For example, δ(constant?, 4) = true. The
rule [REF] for (ref v) creates a new reference cell by extending thestore S with a triple “(x, y) 7→ v”, where v is the initial value ofthe cell, and x and y are binding occurrences for functions that read
and write the value of this cell via the [GET] and [SET] rules, respectively.
The last four rules of the CSI machine add inter-module interactions, in a manner analogous to remote procedure calls. Specifically, the code term C may contain free variables not bound in thestore S; these free variables are external references to functions defined by other modules. The CSI machine communicates with theseother modules via an event stream.
The CSI machine does not transmit λ-expressions themselves;
instead, each transmitted value is first translated into a handle,
which is either a constant or a fresh variable. The following operation I[h . v] performs the appropriate translation of a value v intoa handle h, and returns an appropriately updated interface component. Constants c are transmitted by-value, and functions (λy. e)
and imported variables y are transmitted by exporting a fresh variable z that is bound by I to that value. As usual, I[z 7→ v] denotes
a function that is identical to I except that it maps z to v.
I[c . c]I[z . (λy. e)]
I[z . y]

def

=
def
=
def
=

I
I[z 7→ λy. e]
I[z 7→ y]z freshz freshIn a function application E[x v] where x is externally defined,
the rule [SEND - CALL] first translates the argument value v into an
external handle h via the operation I[h . v], and then transmits theevent send.call(x, h).
After transmitting the event send.call(x, h), the module becomes inactive or quiescent, with code E[send.callx ⊥] indicating that the module is waiting for a matching return rcv.ret(x, h0 ),after which evaluation continues with E[h0 ]: see [RCV- RET].

Figure 1: CSI Machine
Domains
State

CSI

∈

Code × Store × Interface

Code
Store
Interface

C
S
I

::=
∈
∈

E[e] | Q[⊥]
P(Var × Var × Value)
Var → Value

Evaluation context
Quiescent context
Value
HandleEvent
Direction
Trace

E
Q
v
h
a
ρ
t

E[• e] | E[v •] | E[ref •] | Q[rcv.callx •]• | E[send.callx •]c | x | λy. ec|x
ρ.ret(x, h) | ρ.call(x, h)send | rcv
~a

::=
::=
::=
::=
::=
::=
::=

Transition relation (→) ⊆ State × Event ⊥ × State
h
h
h
h
h

E[(λx. e) v],
E[c v],
E[ref v],
E[x v],
E[y v],

S,
Ii
S,
Ii
S,
Ii
S[(x, y) 7→ v 0 ], I i
S[(x, y) 7→ v 0 ], I ihE[x v],
hE[send.callx ⊥],hQ[⊥],h Q[rcv.callx v],

S,
S,
S,
S,

Ii
Ii
Ii
Ii

→
→
→
→
→

h
h
h
h
h

E[e[x := v]],E[v 0 ],
E[pair x y],
E[v 0 ],
E[v],

S,
S,
S[(x, y) 7→ v],
S[(x, y) 7→ v 0 ],S[(x, y) 7→ v],

I
I
I
I
I

i
i
i
i
i

→send.call(x,h)→rcv.ret(x,h)→rcv.call(x,h)→send.ret(x,h)

h E[send.callx ⊥],hE[h],hQ[rcv.callx (v h)],
h
Q[⊥],

S,
S,
S,
S,

I[h . v] i
Ii
Ii
I[h . v] i

[CALL]
v 0 = δ(c, v) [PRIM]x, y fresh
[REF]
[GET]
[SET]
x 6∈ BV(S)
I(x) = v[SEND - CALL][RCV- RET]
[RCV- CALL][SEND - RET]

Figure 2: Example of Linking and Running Two CSI Machines Concurrently
The two CSI machines shown below cooperate to evaluate linkRun([[H]], [[twice]]). After the initial bootstrapping, send events of one machine match rcv
events of the other and vice-versa. The final send.ret(y, 6) event reports the result of the execution is 6.
Evaluation of H = (λt. t (λx. x+1) 4)
I1 = [y 7→ (λt. t (λx. x+1) 4)]
J1 = [y 7→ (λt. t (λx. x+1) 4), f 7→ (λx. x+1)]

Evaluation of twice = (λf. λx. f (f x))
I2 = [t 7→ (λf. λx. f (f x))]J2 = [t 7→ (λf. λx. f (f x)), g 7→ (λx. f (f x))]∅, ∅ i →send.ret(start,y)∅, I1 i →rcv.call(y,t)∅, I1 i →∅, I1 i →send.call(t,f )∅, J1 i→rcv.ret(t,g)
h rcv.cally (g 4),∅, J1 i →send.call(g,4)
h rcv.cally (send.callg ⊥),∅, J1 i→rcv.call(f,4)
h rcv.cally (send.callg (rcv.callf ((λx. x+1) 4))), ∅, J1 i →2h rcv.cally (send.callg (rcv.callf 5)),∅, J1 i →send.ret(f,5)
h rcv.cally (send.callg ⊥),∅, J1 i →rcv.call(f,5)
h rcv.cally (send.callg (rcv.callf ((λx. x+1) 5))), ∅, J1 i →2h rcv.cally (send.callg (rcv.callf 6)),∅, J1 i →send.ret(f,6)
h rcv.cally (send.callg ⊥),∅, J1 i →rcv.ret(g,6)
h rcv.cally 6,∅, J1 i →send.ret(y,6)
h ⊥,∅, J1 ih rcv.callstart (λf. λx. f (f x)), ∅, ∅ i→send.ret(start,t) h ⊥,∅, I2 ih rcv.callstart (λt. t (λx. x+1) 4),h ⊥,h rcv.cally ((λt. t (λx. x+1) 4) t),
h rcv.cally ((t (λx. x+1)) 4),
h rcv.cally (send.callt ⊥) 4),→rcv.call(t,f )→→send.ret(t,g)→rcv.call(g,4)→→send.call(f,4)

h rcv.callt ((λf. λx. f (f x)) f ), ∅, I2 ih rcv.callt (λx. f (f x)),∅, I2 ih ⊥,∅, J2 ih rcv.callg ((λx. f (f x)) 4),∅, J2 ih rcv.callg (f (f 4)),∅, J2 ih rcv.callg (send.callf (f ⊥)), ∅, J2 i

→rcv.ret(f,5)→send.call(f,5)

h rcv.callg (f 5),
h rcv.callg (send.callf ⊥),∅, J2 i∅, J2 i→rcv.ret(f,6)→send.ret(g,6)

h rcv.callg 6,h ⊥,∅, J2 i∅, J2 iSince the code component encodes both active and quiescentstates, we define both standard evaluation contexts E and quiescentcontexts Q. A code component of Q[⊥] means that control is external to the module, but the module can still receive external calls
via a rcv.call(x, h) event. Here, x should be some previously exported function whose definition v is defined by I, and evaluation
continues with Q[rcv.callx (v h)], as described by [RCV- CALL].
Once (v h) reduces to a value v 0 , the rcv.callx marker indicatesthat control should return to the caller module via [SEND - RET].
For a module e, we initialize its execution with the code
(rcv.callstart e), where start is an artificial variable name denoting the initial evaluation of a module. Once the evaluation of eterminates, it will return send.ret(start, h) and wait for incoming
events. The meaning of a module e is then the set of all possible
event sequences ~a that e can generate under the CSI machine:
[[−]]
[[e]]

Module → P(Trace){~a | hrcv.callstart e, ∅, ∅i →~a CSI }:=We use t to range over traces or finite event sequences ~a; we use
T to range over sets of traces; and t · t0 to denote trace concatenation. The exported variables (EV ) and imported variables (IV ) ina CSI machine state, and the bound variables (BV ) of a store S,
are:
def

EV ( C, S, I )IV ( C, S, I )

=
def
=

BV (S)=defdom(I)(F V (C) ∪ F V (rng(S)) ∪ F V (rng(I)))\ BV (S){x, y | S contains (x, y) 7→ v}

Thus, the initial state hrcv.callstart e, ∅, ∅i of a module’s computation has no imported variables or capabilities [37]; they must be
passed explicitly as arguments to functions defined by the module.
3.2

Suppose a program consists of a single module e, which performs
some computation and then returns a final result, with no subsequent interactions. We assume that the result is first-order data (i.e.,a constant) since a function result would be opaque and thus meaningless. The following function run(T ) extracts from the trace set
T = [[e]] the result of running the program e, which is simply theconstant it returns.
def

=

def

linkRun(T1 , T2 ) ={c | send.ret(start, h) · t2 ∈ T2
send.ret(start, x) · rcv.call(x, h) · t2 · send.ret(x, c) ∈ T1 }Here, trace set T2 (for the function argument) starts by returning ahandle h. Trace set T1 returns a function x that is then immediately
applied to handle h from T2 . Subsequent events from the two
trace sets must then correspond, with each send event from T1
matching a receive event from T2 , and vice versa. Eventually, after
the function x completes its computation and its interaction with its
argument h, trace set T1 finally returns a result c. We assume that
this result is first-order data (i.e., a constant) since a function result
would be opaque and thus meaningless.
3.4{c | send.ret(start, c) ∈ T }Thus, we run a program e by starting the CSI machine in statehrcv.callstart e, ∅, ∅i and run its computation until it emits asend.ret(start, c) event containing the result of that computation.
Linking Two Modules

More generally, a program may consist of multiple (reactive) modules that must be linked before running. For simplicity, we consider
the case where the program consists of just two modules e1 and e2 ,where the module e1 is a function that expects the result of e2 as anargument. Subsequently, the two modules may continue to interact
by communicating events, where every send event of e2 becomesa rcv event by e1 , and vice versa. More generally, every event aof e2 must match a dual event a of e1 , where the dual operation
ρ on directions swaps sends and receives, and this dual operation
extends in a compatible manner to events and to event sequences:def

send = rcv

defrcv = send

Semantic Equivalence

We now have two notions of module linking. We can link two
modules e1 and e2 via function application, and run the resulting
expression (e1 e2 ) on a single CSI machine according to run.
Alternatively, we can run e1 and e2 on separate CSI machinesthat communicate according to linkRun. The following theorem
proves that these two notions coincide, which implies that linkRun
correctly captures our notion of module composition as function
application:
T HEOREM 1 (Module Transparency). For any closed expressions
e1 and e2 , linkRun([[e1 ]], [[e2 ]]) = run([[e1 e2 ]]).
P ROOF : By proving a bisimulation relation between the CSI machine state of run and the CSI state pairs of linkRun. 
3.6

3.3

ExampleTo illustrate module linking, Figure 2 revisits the (H twice) example to show how each module can run on a separate CSI machine,using the function linkRun to link up the event traces from these
two machines. In particular, the handle t returned by the evaluationof twice is passed as the argument to the function y produced by
the evaluation of H. Subsequent events from the two modules mustmatch exactly, with each send event from one module matchinga corresponding rcv event from the other module. Finally, the H
module returns the constant 6 as the result of applying y to twice;thus 6 is the final result of running this program.
For this test harness, the module twice produces the trace
shown in the right column of Figure 2. However, twice can generate many additional traces if linked with other modules. The trace
set [[twice]] captures the set of all possible traces generated by the
CSI machine when executing twice.
3.5

Running a Single Modulerun(T )

Based on this dual operation, we formalize the notion of linking
and running two trace sets T1 and T2 (where Ti = [[ei ]]) as follows:

Well-Formed Traces

An inspection of the CSI machine reveals that it generates traces
satisfying the following structural and scoping properties; we referto such traces as being well-formed.
1. Traces consist of alternating send events, which produce a quiescent state, and receive events, which re-initiate computation.
2. Every send.ret(x, h) matches a preceding rcv.call(x, h0 ),and every rcv.ret(x, h) matches a preceding send.call(x, h0 ),so these events form “balanced bracket pairs”, with the exception of the initial send.ret(start, h) that starts each trace.
3. Exporting a variable x via send.call(y, x) or send.ret(y, x)
adds x to the interface I, where it is in scope for subsequentrcv.call(x, h) events.

4. Importing a variable x via rcv.call(y, x) or rcv.ret(y, x)means that x occurs free in the CSI machine and can be used insubsequent send.call(x, h) events.
Properties 3 and 4 provide an implicit notion of variable scoping, where the second variable in each event is a binding occurrence, and the first argument must be a bound occurrence. We consider two traces to be α-equivalent if they are identical modulo consistent renaming of bound variables, and we implicitly perform αconversion to avoid name collisions.
The set T of traces generated by the CSI machine also satisfies
the following properties:
1. It is prefix-closed.
2. It is input-enabled, in that whenever it can receive one event it
is willing to receive any well-formed event: if t.a ∈ T , a and a0
are both receive events, and t.a0 is well-formed then t.a0 ∈ T.

4.2

Copycat Traces

We next consider contracts that are more restrictive than the identity
function. Suppose the target module e generates the trace:t = send.ret(start, h) · a1 · . . . · an
If the contract K permits this trace then [[eK ]] should include:def

copycat(t) =send.ret(start, f ) · rcv.call(f, h) · send.ret(f, bh)·copy(a1 ) · . . . · copy(an )This trace returns a function f that is applied to the handle h
produced by t. It then returns a renamed handle bh, and subsequently
copies every event ai from one side of eK to the other via thefollowing event copying function copy(a):3. It is output-deterministic, in that at most one send event ispossible at any point. Thus, if t.a ∈ T , t.a0 ∈ T , and a anda0 are both send events, then a = a0 .

copy(send.call(y, h))copy(send.ret (y, h))copy(rcv.call(y, h))copy(rcv.ret (y, h))4.

We extend copycat from traces to trace sets in a pointwise fashion:

Contracts as Trace Predicates

The CSI machine semantics exposes each module’s behavior as a
trace set. We now use this formalism to study contract enforcement.
Consider a module e whose behavior is the set of traces [[e]].
Each trace represents a behavior that could be observed on a particular execution. A contract is a mechanism for restricting the setof observable behaviors to those satisfying some safety predicate.
Formally, a contract is a set of traces K ⊆ Trace that is prefixclosed, computable, and that contains only well-formed traces. The
execution of e under contract K should only generate traces in theintersection K ∩ [[e]]. Since K restricts both rcv and send events,
it explicates e’s assumptions and guarantees.
For a contract K, we want to implement a function eK thattakes as argument the module e. The function eK then observes
all of e’s behaviors and halts program execution if any of thosebehaviors violate K. Thus, eK should satisfy a requirement like[[eK e]] = K ∩ [[e]]. However, [[eK e]] must be input-enabled but K(and hence K ∩ [[e]]) may not be input-enabled, so more precisely[[eK e]] should be the input-enabled closure of K ∩ [[e]], that is,
the smallest superset of K ∩ [[e]] that is input-enabled. Intuitively,[[eK e]] has to receive “bad” events from its enclosing context but
can block them from being sent on to e.
4.1

The Universal Contract

The identity function (λx. x) behaves like a universal contract, inthat ((λx. x) e) exposes all the behaviors of module e. We start bystudying the semantics [[λx. x]] of this universal contract.
Consider the possible executions of the CSI machine startingfrom the initial state S0 = hrcv.callstart (λx. x), ∅, ∅i. Whenever the machine imports a variable y via [RCV- CALL] or [RCV- RET],
it immediately exports a fresh name, say yb, for that variable, via[SEND - CALL] or [SEND - RET]. Here, the hat (b· ) operator maps between imported and exported variable names, and is an involution(its own inverse). We extend this hat operator to handles by defining ĉ = c. The set of identity function traces [[λx. x]] is then thewell-formed subset of the prefix-closure of the following regular
grammar. Note that the last two productions essentially copy eventsfrom one side of the identity function to the other, renaming variables appropriately.
Tid

::=
|
|
|

send.ret(start, f )Tid · rcv.call(f, h)·send.ret (f, bh)Tid · rcv.call(y, h)·send.call(by, bh)Tid · rcv.ret (y, h)·send.ret (b
y, b
h)

=
=
=
=

rcv.call(y, h)·send.call(by, bh)rcv.ret (y, h)·send.ret (by, bh)rcv.call(by, bh)·send.call(y, h)
rcv.ret (by, bh)·send.ret (y, h)def

copycat(K) = {copycat(t) | t ∈ K}
This copycat function allows us to formalize the relationship between the permissible traces K and the contract implementation
eK . We require that eK copies only K-traces:[[eK ]] is the prefix and input-enabled closure of copycat(K)5.

The Programmatic Monitor Interface

Based on the above specification, it is possible to hand-code an
implementation eK for each contract K, but these implementations
are difficult to read and write, and can violate non-interference.
Instead, we propose to express eK as a pair of a guard anda monitor. The predefined guard function performs the necessary copycat behavior on event streams and guarantees noninterference. It also encodes the observed event stream and communicates it to the monitor M , which detects errors and reports
them to the guard, which then halts execution. Thus, we implement
eK as:
def

eK = (guard M )Traces contain scope and binding information, which is tricky
to communicate to the monitor M . Our chosen encoding is that,when an event such as rcv.call(·, x) introduces a new variable
x, the monitor M creates two new sub-monitors, say Mcall andMret , which handle events ρ.call(x, ) and ρ.ret(x, ), respectively. This encoding avoids passing function references (or getters/setters for mutable reference cells) to M , which helps ensure
non-interference. We also require that the monitor M is closed, sothat it does not gain accesses to function references through its environment.
Based on this discussion, the type τ of the monitor M is:τ = (Constant → Bool ) × (Unit → (False + (τ × τ )))When an event transmits a constant, the first component of M iscalled to decide if that event is permitted. That function can use
mutable internal state to track and enforce temporal properties.
Thus, temporal properties of the contracts are implemented via
imperative state in the monitor.
When an event transmits a function x, the second componentof M is called, which again has the opportunity to halt execution
by retuning false. Otherwise, the function should return a pair ofmonitors for handling call and ret events on the function x.

The function guard below then converts its monitor argument
M into an appropriate contract implementation that queries M toverify that each transmitted event is permitted:

1

deepTrace = (helper "send" "rcv" "ret" "start")2

helper send rcv op fn =pair (λx. print (send+"."+op+"("+fn+","+x+")")
5
true)
6
(λ. let name = gensym()
7
print (send+"."+op+"("+fn+","+name+")")
8pair (helper rcv send "call" name)9(helper send rcv "ret" name))

3
4

guard M =λx. if (constant? x) then3
assert ((fst M) x) != false
4
x
5
else
6
let MM = (snd M)()
7
assert MM != false8
λy. (guard (snd MM) (x (guard (fst MM) y)))
1
2

5.3
5.1

Example Monitors

Using the monitor interface, it is straightforward to implement auniversal monitor Any that permits all communication:
rec Any = pair (λx. true) (λ. pair Any Any)
As a more interesting example, the following code shows how
to implement revokable membranes [37]. In this code, ref true
returns a pair of get and set methods. As long as get() returns
true, the monitor M behaves like the universal contract. Calling
revoke puts false into the reference cell, after which all further
communication is prohibited. The top-level membrane function
returns a pair of the membrane monitor and its revoke function.

Non-Interference and Trace CompletenessWe now revisit the design goals of non-interference and trace completeness, to show how they are achieved by the guard/monitor architecture.
First, for any monitor M , the function (guard M ) satisfies noninterference, in that it behaves like the identity function except thatit may abruptly halt certain (erroneous) executions. Thus, guard
behaves like an “information diode”, in that information can flow
into the monitor M but can never flow back out to the program. In
a richer language with exceptions, guard would need to appropriately catch any thrown exceptions to ensure that they do not constitute an additional information channel between the monitor andthe enclosing program.
T HEOREM 2 (Non-Interference). For any closed expression M ,membrane =2
λ. let (get,set) = ref true3
let revoke= λ. set false
4
letrec M= pair (λx. get())
5(λ . if (get())
6then (pair M M)
7else false)
8
in pair M revoke
1

Note that M is not strictly speaking a monitor, since it calls a freevariable get, which could (in theory, but not in this case) interferewith the enclosing program.

[[guard M ]] ⊆ [[λx. x]]
P ROOF : By showing that the trace set [[λx. x]] from section 4.1 isa superset of [[guard M ]]. The behavior of M is irrelevant, since
non-interference is guaranteed entirely by guard. 
Our argument for trace completeness is based on showing thatthe monitor observes all events that cross the contract boundary.
Specifically, consider the semantics of an arbitrary module e under
the deepTrace monitor, i.e.,[[(guard deepTrace) e]]

5.2

Deep Tracing

A particularly interesting monitor is deepTrace, which performs“deep” or higher-order tracing. The code ((guard deepTrace) g)
prints all calls and returns of g. Additionally, if g takes or returns
functions, then those functions are also traced. Thus, deep tracing
reports both first-order and higher-order interactions between themodule g and the rest of the program.
Revisiting the example twice from Section 3.4, the program

An investigation of the reachable states of the corresponding CSI
machine shows that this module prints each send event before
transmitting it, and prints each rcv event right after receiving it. Instead of printing these events, deepTrace could feed them into analgorithm that decides a computable contract K over event traces,
and could halt execution once that algorithm detects a trace that violates K. Consequently, any computable predicate over traces could
be implemented using the monitor interface.

(H ((guard deepTrace) twice))
5.4
prints out the event sequence shown in the right half of Figure 2(modulo naming of bound variables). Alternatively, the program(((guard deepTrace) H) twice)prints out the event sequence shown in the left half of that figure.
In this manner, deep tracing allows the programmer to observe thetrace semantics of a module as explored during a particular run.
The implementation of deepTrace uses an auxiliary function
helper to generate the appropriate monitor. The helper function
takes four arguments: the first two indicate whether this monitor isobserving send or receive events; the third whether it is receiving
ret or call events; and the fourth argument is a function name.
Every function that passes through the guard is assigned a newname via gensym, and the generated monitor then prints each event.

Dependent Contracts

Dependent contracts allow a function’s range contract R to dependon the function’s argument x. If the argument x is itself a function,then R could violate non-interference by calling x.
Our guard/monitor architecture avoids this difficulty by only
allowing dependency when the argument x is a first-order value(that is, a constant). Essentially, the argument x is saved on astack by the domain contract, and is then popped by the matchingrange contract. The following monitor illustrates how to implement
such dependent contracts. It specifies a function contract where
the integer result should be greater than the integer argument. The
monitor accepts only functions, where the function’s argument x
must be an integer constant that is pushed on a stack that records
the arguments of currently active calls, and the function’s result ymust be an integer that is greater than the argument.

increasingMonitor =let (push,pop) = newStack()3
pair (λx. false) // no constants allowed4(λ. pair (pair (λx. (push x); (integer? x))
5(λ. false))
6(pair (λy. (integer? y) && y > pop())
7(λ. false)))1

Figure 3: Declarative HOT Contracts

2This explicit stack design also avoids subtle difficulties withblame assignment in traditional dependent contracts [15].

6.

M ::= S where R
S ::= flat(e) | n : S1 7→ S2
R ::= A | !A | RR | R∗ | not R | R ∪ R| . . . | call(n, ?x) R | ret(n, ?x) R
A ::= call(n, p) | ret(n, p)
p ::= | x | cn ∈ Name

HOT contract
Structural contract
Temporal contract
Event patterns
Value patterns
Function names

Blame Assignment

The discussion so far has focused on detecting contract violations;
we next address how to assign blame for these violations. In particular, we show that blame assignment, previously studied in higherorder contract systems [19], extends in a consistent fashion to themore general setting of temporal higher-order contracts.
Suppose the program consists of two modules e1 and e2 , withcorresponding trace sets Ti = [[ei ]] for i ∈ 1, 2, and suppose that K
is a contract on e2 . The semantics of correct executions is definedas:linkRun(T1 , K ∩ T2 )This formula links together the modules e1 and e2 , with the requirement that all interaction between the two modules must be
permitted by K.
We now extend that semantics to assign blame, via the function
linkMonitorRun(T1 , K, T2 ) shown below. The first case in thisdefinition is analogous to the function linkRun defined earlier, withthe additional requirement that the trace send.ret(start, h) · t2 in
T2 must be permitted by K. The second case deals with assigning
blame, where T1 and T2 want to exchange a message a that is not
permitted by K, but where the prefix of a is accepted by all parties.
In this situation, the module i sending that message is blamed.

7.

The Declarative Contract Language

The programmatic monitor interface provides trace completeness,
non-interference, and blame assignment. We now leverage that interface to develop a declarative contract language for writing mixed
higher-order temporal (HOT) contracts. Our declarative language
sacrifices trace completeness for ease-of-expression, but still interoperates with the monitor interface for situations where additional
expressiveness is required.
Figure 3 summarizes the contract syntax. A HOT contract
S where R

contains both a structural component (S) that binds function names(n), and a temporal component (R) that imposes constraints on
when those functions can be called or return.
The flat structural contract flat(e) describes the set of constantsc that satisfy the predicate e. The higher-order structural contract(n : S1 7→ S2 ) describes functions where S1 and S2 specify thefunction’s domain and range contracts, respectively, and n provides
a name for this function that can be referenced in the temporalcomponent.
In the temporal component, event patterns call(n, p) andret(n, p) denote calls and returns of the function named n, wheredefthe argument or result matches pattern p. Patterns include conlinkMonitorRun(T1 , K, T2 ) =stants, variables x, and “ ”, which matches any argument.
{c | send.ret(start, h) · t2 ∈ K ∩ T2
Temporal contracts (R) include events (A), negated events
send.ret(start, x) · rcv.call(x, h) · t2 · send.ret(x, c) ∈ T1 }(!A), concatentation (RR), Kleene closure (R∗ ), negation of trace∪ {blame i | send.ret(start, h) · t2 · a ∈ T2
sets (not R), union (R ∪ R), and the universal temporal contract
send.ret(start, x) · rcv.call(x, h) · t2 · a ∈ T1(“. . . ”), which matches any trace. Temporal contracts also includesend.ret(start, h) · t2 ∈ Kdependent sequencing patterns such as call(n, ?x) R, where thesend.ret(start, h) · t2 · a 6∈ K
argument
from the first event is bound to x, and can be referred
if |t2 | odd then i = 1 else i = 2 }to from within R. Dependent sequencing captures common constraints on function arguments and returns, for example, that theThus linkMonitorRun(T1 , K, T2 ) extends linkRun(T1 , K ∩ T2 )argument passed to free must previously have been returned fromto return a blame label in situations where linkRun would failalloc.
silently.
To incorporate blame assignment into the guard implementa7.1 Semantics of HOT Contracts
tion, we introduce additional arguments to track the module andenclosing context of each monitor, where these two arguments are
To formalize the semantics of a structural contract S, we define answapped for contravariant domain checks (as in [19]). We assume aabstract machine called the EF machine that describes what traces
primitive blame for reporting blame, and an appropriate represenS permits.
tation for module labels (e.g., strings).
This EF machine contains an environment E and a stack F .
The environment E associates each variable x with a direction
1 guard module context M =ρ (describing whether x was sent or received) and a structural2
λx. if (constant? x) thencontract S (describing permitted uses of x). The stack F contains
3
if ((fst M) x) == false then blame module
the variable names of inter-module calls (or stack frames).
4x
E ::=  | E, x : ρS
5else
F ::= Variable ∗6
let MM = (snd M)()7
if MM == false then blame module
The EF machine generates traces according to the following
8
λy. (guard module context (snd MM)transition relation EF ⇒a EF 0 . The stack length |F | indicates9(x (guard context module (fst MM) y)))whether the contracted module is active or quescient, so if |F | is
odd we require that ρ = send, and otherwise that ρ = rcv, in both

7.2of these rules.
hE, F i⇒ρ.call(x,h)

hE ⊕ (h : ρS1 ), F.xi
where E(x) = ρ(n : S1 7→ S2 )[S - CALL]

hE, F.xi⇒ρ.ret(x,h)

hE ⊕ (h : ρS2 ), F i
where E(x) = ρ(n : S1 7→ S2 )[S - RET]

Assuming ρ = send, the rule [S - CALL] generates a call event
send.call(x, h), provided x was previously received and has afunction contract. (If ρ = rcv then the dual situation applies.) The[S - RET] rule generates a return event that must return to the top
variable on the stack F .
The operation E ⊕ (h : ρS1 ) checks if a sent handle h is compatible with the argument contract S1 , and extends the environment
E appropriately. Note that the check run([[e c]]) = true ensuresthat the constant c satisfies the structural contract flat(e).
E ⊕ (c : ρ flat(e))
E ⊕ (x : ρS)==

EE, x : ρSprovided run([[e c]]) = true

The meaning of a structural contract S is then defined as theset of all traces that first return a handle satisfying S, and where
subsequent interactions satisfy the requirements of the EF machine:
[[S]]

=

{ send.ret(start, h).t | hE0 , starti ⇒t hE, F i }where E0 = ∅ ⊕ (h : send S)

The meaning of a temporal contract R is defined with respect
to the environment E that is produced by the EF machine, where
E is used to map each variable x in the trace to a name n that isreferenced in the temporal contract. The relation p ∼ h defines
when a pattern p matches a handle h. Constants match constants(c ∼ c), and the pattern “ ” matches any handle ( ∼ h).

Compiling HOT Contracts

We enforce each contract (S where R) by compiling it into an
appropriate monitor. We convert the temporal component R into a
finite state automaton, where s ranges over the state space of theautomaton, s0 denotes the initial state, and the handlers calln andretn for each function name n imperatively update s appropriately
and return true if the automaton is in an accepting state and false
otherwise. The code is roughly:
let s
= s0
calln = λi. · · · check and update s appropriately · · ·
...
...
retn
= λo. · · · check and update s appropriately · · ·...
...
in compile(λx.true, S)
The function compile(f, S) generates a monitor that ensuresthat the trace satisfies S, and which is parameterized over a numberof calln and retn functions that communicate to the temporalcode above. The additional argumentf : (Constant ∪ {λx.x} 7→ Bool )is an “observer function” that is called and can signal an error
whenever a value passes through this S boundary; it is used in thefollowing recursive definition of compile.
compile : (Constant ∪ {λx.x} 7→ Bool ) × S 7→ Monitor
defcompile(f, flat(e)) =pair (λx. (e x) && (f x))(λ. false)defcompile(f, n : S1 7→ S2 ) =pair (λx. false)(λ. (f (λx.x)) && (pair compile(calln , S1 )compile(retn , S2 ))))
defcompile(f, y) =let (chkconst,chkfn) = ypair (λx. (f x)&& (chkconst x))(λ. (f (λx.x)) && (chkfn()))[[•]]• : R × E → P(Trace)
For the contract flat(e), the generated monitor accepts only[[call(n, p)]]E = {ρ.call(y, h) | E(y) = n : . . . and p ∼ h}constants; it checks that the constant satisfies both the observer[[ret(n, p)]]E = {ρ.ret(y, h) | E(y) = n : . . . and p ∼ h}function f and the predicate e. For the function contract n : S1 7→[[!A]]E = Event \ [[A]]E
S2 , the generated monitor accepts only functions. It immediately[[R1 R2 ]]E = [[R1 ]]E · [[R2 ]]E
notifies the observer that a function is passing through this contract,[[R∗ ]]E = [[R]]∗E
and then returns a pair of monitors that monitor calls and returns of[[not R]]E = any trace \ [[R]]E
this function, in each case notifying calln or retn and enforcing[[R1 ∪ R2 ]]E = [[R1 ]]E ∪ [[R2 ]]E
the sub-contracts S1 or S2 , as appropriate.
[[ . . . ]]E = any trace
Our implementation extends the structural contract language to[[call(n, ?x) R]]E = {ρ.call(y, c) · t | E(y) = n : .., t ∈ [[R[x := c]]]E }[[ret(n, ?x) R]]E = {ρ.ret(y, c) · t | E(y) = n : .., t ∈ [[R[x := c]]]E } include variable references (y) for referring to predefined monitors
such as the Any monitor defined in section 5.1. The compilation ofsuch monitor references extends the referenced monitor to call the
Finally, the meaning of a contract (S where R) is defined as
observer function f appropriately.
any trace that satisfies S, providing a resulting environment E, andCompilation Correctness The compile function compiles awhere the trace also satisfies R with respect to E. The function
structural contract S into a monitor in a manner than respects theprefixes performs prefix-closure on a set of traces.
intended meaning [[S]] of the structural contract.
[[S where R]]def= { (send.ret(start, h) · t) ∈ prefixes([[R]]E ) |hE0 , starti ⇒t hE, F i and E0 = ∅ ⊕ (h : send S) }Thus, a module e under contract S where R yields the trace set:[[e]] ∩ [[S where R]]

T HEOREM 3 (Compilation Correctness). For any structural contract S, [[S]] = [[guard compile(λx.true, S)]].
P ROOF SKETCH : We proceed by structural induction on S.
In the case that S = flat(e): we substitute into the theorem,
then focus on the right-hand side. We expand the definition ofcompile and do beta reduction. The application of (f x) in thedefinition reduces to true with the given f , so we remove it andthe and-expression. This and an application of eta produces theright-hand side: [[guard (pair e (λ.false))]]. If we expand thisapplication of guard, it only succeeds if the value sent to thecontract is a constant, c, such that (e c) evaluates to true. We now
focus on the left-hand side. By expanding the definition of [[S]] and⊕, we get the condition that run([[e c]]) = true where c is theconstant sent to the contract. Clearly these two constraints are thesame, so this case is completed.
In the case that S = n : S1 7→ S2 , we use the inductive
hypothesis twice. However, getting to that point requires a few
subtle steps. First, we assume that calln and retn are λx.true
for all n, since we are only considering structural contracts, so
there are no temporal properties to enforce. Next, we consider the
behavior of both sides after it has been applied. Only the casewhere it is actually a function is relevant, because if it is a constant,both trivially reject any subsequent events. After assuming we’ve
received a function, we then assume that the function is called andreturns. The contracts S1 and S2 protect the call and return throughthe S-C ALL and S-R ET rules on the left and through the recursive
calls to guard on the right—and the inductive hypothesis ensuresthat these have identical semantics. It is often safer to enumerate “bad” behavior, so that all unmentioned good behavior is allowed—including good behavior not yet
implemented. The following contract reads, “Do not call acquire
twice without an interleaving release, and do not call release
twice without an interleaving acquire.”

Compiling Dependent Sequences For dependent sequences, wefollow the same general approach, except we cannot compile to a
finite state automaton. For example, the constraint

This version is extensible, because our use of event negation
matches functions that have yet to be written. Unfortunately, it
constrains future versions of the module so that acquire must
be the first call. If we simply rotate the sequence, we avoid thatproblem:not ... call(free,?z) !ret(alloc,z)* call(free,z)requires unbound storage to record all freed locations z. Instead, we
compile to a lazily constructed infinite automaton. Each automaton
is a function from an event (call or return) to a next automaton—
as well as a boolean to encode acceptance. Event patterns arefunctions that return the epsilon automaton on matching and a null(rejecting) automaton otherwise. In contrast, dependent sequences
return a new automaton representing the rest of the trace, and which
includes an appropriate binding for the dependent variable z.
Each of the regular grammar operators (sequencing, complement, etc) is implemented as an explicit automaton that simulates
the operator using the automaton functions representing its pieces.
These implementations correspond precisely to the intuitive explanations of regular operator closure properties found in any textbook
on automata theory. Since Kleene star and sequencing may invoke
their arguments multiple times, dependent sequences embedded inthem will be duplicated for each successful match of the pattern.
This approach is similar to regular expression derivatives [9, 38].
7.3

ExamplesSection 2 presented a variety of examples of structural/temporalcontracts, whose meaning and compilation can now be understoodbased on the formalism of this section. In particular, the contract
combinator “Pair S 1 S 2 ” abbreviates the contract for Churchencoded pairs “(S 1 → S 2 → Any) → Any”, and generalizes
to a Record combinator that supports n-ary tuples.
The specification of temporal properties involves some subtleties, which we illustrate by considering various contracts for alock object with acquire and release methods. Our initial contract states that acquire and release are atomic, and calls must
alternate between these functions, with acquire being called first.
LockContract =Record acquire : Unit → Unit
release : Unit → Unit
where ( call(acquire,_) ret(acquire,_)call(release,_) ret(release,_) )*This contract states the “good” behavior of this module. This kindof specification is not stable under extension, since adding andcalling other methods from this module would violate this contract.

where not ... call(acquire,_)!call(release,_)* call(acquire,_)and not ... call(release,_)!call(acquire,_)* call(release,_)We must include the initial “...” in the negations, because otherwise we are only disallowing traces that start with the illegal sequence.
Unfortunately, this contract does not specify that acquire must
be called first. We rephrase the property as “After calling acquire,
you may not call it again until you call release, after which you
may not call release and so on.”:where ( call(acquire,_) !call(acquire,_)*call(release,_) !call(release,_)* )*where ( !call(release,_)*!call(acquire,_)*call(acquire,_)call(release,_) )*This version reads, “It is illegal to call release until you acquire,and you may not call acquire twice before calling release.” Notethat this specification constrains only the client, not the lock object
itself. We conjoin the following atomicity requirement to complete
our specification.
and not ... call(acquire,_) !ret(acquire,_)and not ... call(release,_) !ret(release,_)8.

Implementation

Our presentation so far addresses an idealized language. To evaluate this approach in practice, we have extended and implemented
this design for the Racket programing language [22]. Our implementation includes both the programmatic monitor interface from
Section 5 and the declarative HOT contract language of Section 7.
Guard/Monitor Implementation Racket already provide a higherorder contract system with a variety of contract combinators thathave been widely used to document Racket’s libraries, but which
do not support temporal properties directly.
Racket also provides a programmatic make-contract interface, which creates a contract from a user-provided projection function eproj that is expected to satisfy the requirement[[eproj ]] ⊆ [[λx. x]] (ignoring blame issues for simplicity). Since
make-contract does not check that eproj is actually a projection,
it cannot guarantee non-interference.
Our implementation uses this make-contract interface as afoundation on which to implement our guard/monitor architecture.
This design allows monitors to interoperate with the Racket language and to annotate module boundaries, while also guaranteeing
non-interference.
Our implementation addresses a number of additional issues notconsidered in the λ-caculus model. For example, the presence offirst-class continuations allows functions to return multiple times,
or never return, and so the resulting event traces do not satisfy thewell-bracketed property. In order to properly match calls and returns, call events include a unique label, which is then repeated ineach matching return event. The implementation works seamlessly
with mutation, allowing monitors to interpose between accesses
and updates to mutable structures—which are just differentlylabeled events in the trace grammar. The implementation’s monitors are safe with respect to concurrent interaction via a kill-safe
manager thread [21].
Declarative Contract Implementation Our HOT contract language and implementation are almost exactly as described in section 7.2, although the implementation is more general. In particular,
as well as the structural contract forms of section 7.2, it also accepts Racket’s previous non-temporal contract language (wherethese contracts do not produce events for the temporal portion).
We also provide a facility for defining macros to abbreviatecommon temporal constraints, such as the following atomic andtransient macros. A function is atomic if it returns immediately after it is called, with no intermediate interactions that are visible
to the contract; meaning no interactions to explicitly labeled functions, since we do not do deep-tracing by default:
atomic(f)def=not ... call(f,_) !ret(f,_)

A higher-order argument g is transient when passed to a function
f if g can only be called before f returns—that is, f does not get apermanent capability to call g, but only a transient capability.
transient(g,f)

def=

not ... ret(f,_) ... call(g,_)

The syntax R1 ∩ R2 is introduced via a macro that expands tonot (not R1 ) ∪ (not R2 ). Other macros including optional events,
bounded-length sequences, etc.
Performance Evaluation The performance overhead of contracts
depends critically on the amount of work performed by the application within a contract boundary. To avoid this application dependence, we compared the performance of temporal contracts
with Racket’s current contract system using the following microbenchmark. We applied a contract to the identity function thatchecks for integer arguments and results. The following results
measure the time to call the resulting function 106 times, under
three different contract implementations:• 870ms for Racket’s current contract system.
• 877ms for the new monitor interface.
• 854ms for the HOT contract language.

The results demonstrate that, when the additional expressivenessof temporal contracts is not used, our proposed contract systemprovides equivalent performance to Racket’s current non-temporalcontract implementation. Furthermore, both the programmatic
monitor interface and the HOT contract language provide equivalent performance.
We investigated the overhead of temporal constraints by extending the contract to check that the called function is atomic. The
resulting performance numbers are:
• 931ms for the new monitor interface when enforcing atomicity.
• 1435ms for the HOT contract language when enforcing atom-

icity, using an optimized implementation that does not support
dependent sequencing.
• 2371ms for the HOT contract language when enforcing atomicity, using a more general implementation that supports dependent sequencing.
These results indicate that the monitor architecture provides anefficient mechanism for enforcing simple temporal properties withlittle additional overhead.
Our current implementation of temporal automata for the HOT
contract language is quite general and so a little slow. Restricting

temporal constraints to disallow dependent sequences improves
performance significantly, and we conjecture that other plausible optimizations could achieve performance comparable to themonitor-based implementation. In theory, it should be possible tooptimize HOT contract patterns to the equivalent hand-coded monitor, at least for common specifications such as atomicity, but thisremains for future work.
Monitoring Filesystem Accesses Experience with Racket’s current contract system indicate its overhead is quite adequate formonitoring the vast majority of APIs, where the work inside thecontract boundary dominates the contract overhead, and so contracts have little impact on performance. We conjecture that many
temporal contracts would similarly have no performance impact.
To evaluate this hypothesis, we modified a GUI text editor to use atemporal contract to monitor its filesystem accesses. As expected,
we found no change in the user experience – in particular, the difference in overall application runtime was unmeasurable in benchmarking runs.
Temporal Contracts for the Standard Library We conducted astudy of 600 functions in the Racket standard library to determine
how many of these function could benefit from temporal contracts.
We found that:• 519 functions in the standard library are intended to be atomic.

For example, the number? predicate may be passed a function
argument, but it is not permitted to call this argument; instead it
should immediately return a boolean result.
• 51 library function are passed transient function argumentsthat the library may call, but only before the library function
returns. Examples include map, build-list, filter. None ofthese library functions are allowed to retain a reference to theargument function after the library function returns.
• 17 library function exhibit the opposite behavior, where they

are passed function arguments that should not be called until
the library function returns. These are in-port, in-producer,
stop-before, stop-after, make-do-sequence,
make-custom-hash, make-immutable-custom-hash,make-weak-custom-hash, compose, procedure-rename,procedure->method, procedure-reduce-arity,
make-keyword-procedure,
procedure-reduce-keyword-arity, negate, curry,
curryr.
• The remaining 13 library functions have quite unconstrained

behavior. Examples include apply, keyword-apply, and 11“sequence” functions that may cause additional function calls(because inspecting a sequence can cause lazy code evaluation
across a module boundary.)
Note that the issue of when a function is called, that is addressedin these temporal specifications, is much more critical in a languagewith imperative state and reactive behavior than in a purely function
language, and our work proposes a means to specify and enforce
these temporal aspects of behavior.
Adversarial Defense The contract examples presented so far areuseful for identifying and localizing defects in well-intentioned
but perhaps buggy code. Contracts are also valuable for enforcing
properties at trust boundaries between modules written by different
principals.
As an example, we developed an implementation of Tic-tac-toe
with adversarial players, where each player provides a function
turn : Board → Board
Here, Board is an abstract data type that provides board-get andboard-set methods, and each player’s turn function is supposedto update the Board by placing an additional mark. The core of
the game places complete confidence in the players to follow therules—namely that they must only take one move and they cannot
place their mark over the other player’s mark—and this assumption
greatly simplifies the implementation of the game core.
Of course, this confidence in each player’s code may be misplaced, due to unintentional bugs as well as intentional violations of
the game rules. To make each untrusted turn function trustworthy,
it is monitored by a temporal contract. For example, the following
contract states that a turn may not contain two calls to board-set.
not ... call(board-set,_,_,_,_) !ret(turn,_,_,_)*call(board-set,_,_,_,_)
Additionally, the board should not observe the same row and column of the board being set twice (by either player) during a game.6
not ... call(board-set,_,?r,?c,_) !ret(game,_)*call(board-set,_, r, c,_)To evaluate this architecture, we wrote a collection of player
functions, including textual and graphical interactive players, noncheating AI players, and cheating AI players. In all cases, thecontracts behave as expected—they catch all cheaters, both humanand AI.
Note that the game core consists entirely of calls to contracted
functions. To evaluate the performance overhead, we measured
the time to play a 7 move game between two deterministic noncheating AI players, both with and without the temporal contracts.
The average running time of 100 runs is:• 247ms for the version without contracts, and• 255ms for the version with contracts.

This example demonstrates a key software engineering benefit
of HOT contracts: the game model can be decoupled from thesecurity policy, simplifying both in the process, while imposing
minimal performance overhead in this case study.

9.

Related Work

Temporal Constraints Temporal constraints are widely understood to be important aspects on a module’s behavior, and priorwork has eloquently argued for modeling software modules asplayers in a formal game [12, 13]. Our event sequences are analogous to the interface automata of prior work, and extend thoseideas to handle higher-order languages by introducing the notionsof variable binding and scope in event sequences. It also addresses
dynamic enforcement rather than static verification.
Runtime Verification Much prior work has addressed runtime
monitoring of system behaviors. The MOP Framework [33] provides a general runtime monitoring framework that supports multiple languages and logics. Aspect-Oriented Programming [29] is atechnique for weaving into an existing program additional functionality, including contract checks on module boundaries. AOP
has been used in tools that enforce temporal properties specified in
LTL, such as Tracematches [39] and J-LO [8]. In other approaches,runtime monitors are synthesized from formal specifications, forexample in PathExplorer [25], Eagle [6], and RuleR [7]. Program
Trace Query Language (PTQL) [23] expresses temporal properties
as SQL-like queries over program traces. Generally speaking, theseapproaches focus on temporal properties and do not provide explicit support for higher-order functions.

Behavioral Contracts Meyer [34, 35, 36] introduced contracts
with Eiffel and its contract-oriented design approach. Since thencontracts have been used to extend static checking [14, 5] and forruntime monitoring of higher-order programs [18]. These investigations have progressed towards more expressive dependent contracts [18, 31, 24, 15]. In contrast, our work moves contract expressiveness in a different—orthogonal—direction where contracts
enforce temporal properties.
Our work explicitly enforces that contracts can only observe,
but not influence, execution (apart from stopping execution on contract violations). Prior work on dependent contracts has been morelax in this regard, including allowing dependent function contracts
to observe the argument value, and even call that value in cases
where it is a function [18, 31]. This interpretation of “contracts ascode” eventually requires that each contract is considered an additional module in the system, with its own blame label [15].
Our usage of the flexibility of Racket contracts to enforce
temporal constraints is unique7 , except in one case: Tov and Pucella [43] implement a contract for affine functions. Of course,
affine-ness—allowing at most a single call—is a temporal property
that is trivially encoded in our DSL. Their implementation approach is neceassarily similar to ours, although it is clearly limited
to a single temporal property.
Game Semantics Much prior work has studied the denotationalsemantics of higher-order languages, often with the goal of developing fully abstract denotational semantics in which observableequivalence implies denotational equivalence. Game semantics has
emerged as an appealing foundation for developing fully abstract
denotational models. For example, fully abstract game semantics
have been developed for PCF [3, 27] or for languages with features such as call-by-value [4], general references [2], and exceptions [11, 30], to name just a few. Compositional game semantics also facilitate compositional verification [1]. Our work draws
deeply on game semantics as a tool to study contract systems andmodule behavior, but follows a different development that starts
with the CSI machine, which provides a connection between operational semantics and game semantics.

10.

Discussion and Future Work

We have presented a programmatic monitor architecture for contracts that satisfies the twin goals of trace completeness (allcomputable, prefix-closed contracts are expressible) and noninterference (contracts cannot influence correct executions). The
architecture also provides precise blame assignment, even for complex temporal properties.
Additionally, we presented a declarative contract language thatcan express a variety of temporal constraints on module behavior
that are common in software systems with imperative state, butthey are often left undocumented. Our contract language provides aconvenient declarative means for explicating these temporal aspectsof library interfaces.
We have formalized our ideas in the context of an untyped language that supports rich interactions between modules, including
mutual recursion, higher-order functions and callbacks, and both
encapsulated and shared imperative state. Extending these ideas
to additional language features is an important topic for future
work. For compound data structures such as lists or arrays, contracts could be enforced eagerly (as with constants) or lazily (aswith functions). In this work, compound data structures are Churchencoded as functions and so checked lazily, but eager checking is aninteresting alternative. Other topics for future work include the de-

6 Alternatively, this property could be enforced by a contract that calls

board-get instead of keeping history information, but that specification
does not guarantee non-interference.

7 Based on a search on the publically available Racket code: the core

distribution and an online package repository.

velopment of temporal contracts for typed languages and the studyof temporal higher-order contracts in a concurrent setting.
Acknowledgements We thank Shriram Krishnamurthi and MichaelGreenberg for valuable comments on an earlier draft of this paper,
Robby Findler for helpful discussions on temporal contracts, andMatthias Felleisen for exploring temporal contracts for game policy
enforcement. We are also grateful to the anonymous reviewers of
ICFP 2011 for their constructive feedback. This material is based
upon work supported by the National Science Foundation underGrants 1016334 and 0905650.

[21] Matthew Flatt and Robert Bruce Findler. Kill-safe synchronization
abstractions. In Programming Language Design and Implementation,
pages 47–58, 2004.
[22] Matthew Flatt and PLT. Reference: Racket. Technical Report PLTTR-2010-1, PLT Inc., 2010. http://racket-lang.org/tr1/.
[23] Simon F. Goldsmith, Robert O’Callahan, and Alex Aiken. Relational
queries over program traces. OOPSLA, pages 385–402, 2005.
[24] Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich.
Contracts made manifest. In POPL, 2010.

References[25] Klaus Havelund and Grigore Rosu. An overview of the runtime
verification tool Java PathExplorer. In Formal Methods in System
Design, 2003.

[1] Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, and C.H. Luke Ong. Applying game semantics to compositional softwaremodeling and verification. In TACAS, pages 421–435, 2004.

[26] Ralf Hinze, Johan Jeuring, and Andres Löh. Typed contracts forfunctional programming. In Functional and Logic Programming(FLOPS), pages 208–225. Springer-Verlag, 2006.

[2] Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract
game semantics for general references. In LICS, pages 334–344, 1998.

[27] J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I,
II, and III. Inf. Comput., 163(2):285–408, 2000.

[3] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full
abstraction for PCF. Information and Computation, 163:409–470,
1996.

[28] Murat Karaorman, Urs Hölzle, and John Bruno. jContractor: A
reflective Java library to support design by contract, 1998.

[4] Samson Abramsky and Guy McCusker. Call-by-value games. In CSL,
pages 1–17, 1997.
[5] Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec#
programming system: An overview. In Construction and Analysis ofSafe, Secure and Interoperable Smart Devices, pages 49–69, 2004.
[6] Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik
Sen. Rule-based runtime verification. In VMCAI, pages 44–57, 2004.
[7] Howard Barringer, David Rydeheard, and Klaus Havelund. Rule
Systems for Run-time Monitoring: from EAGLE to RULER. J Logic
Computation, November 2008.
[8] Eric Bodden. J-LO - A tool for runtime-checking temporal assertions.
Diploma thesis, RWTH Aachen University, November 2005.
[9] Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM,
11:481–494, October 1964.
[10] Manuela Carrillo-Castellon, Jesús Garcı́a Molina, Ernesto Pimentel,
and Israel Repiso. Design by contract in smalltalk. JOOP, 9(7):23–28,
1996.
[11] Robert Cartwright, Pierre-Louis Curien, and Matthias Felleisen. Fully
abstract semantics for observably sequential languages. Inf. Comput.,
111(2):297–401, 1994.
[12] Luca de Alfaro and Thomas A. Henzinger. Interface automata. In
Foundations of Software Engineering, pages 109–120, 2001.
[13] Luca de Alfaro and Mariëlle Stoelinga. Interfaces: A game-theoretic
framework for reasoning about component-based systems. Electr.
Notes Theor. Comput. Sci., 97:3–23, 2004.
[14] David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B.
Saxe. Extended static checking. Research Report 159, Compaq
Systems Research Center, December 1998.
[15] C. Dimoulas, R. Findler, C. Flanagan, and M. Felleisen. Correct blamefor contracts: No more scapegoating. In POPL, 2011.
[16] Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt.
Semantics Engineering with PLT Redex. The MIT Press, 1st edition,
2009.

[29] Gregor Kiczales, John Lamping, Anurag Mendhekar, Chris Maeda,
Cristina Lopes, Jean-Marc Loingtier, and John Irwin. Aspect-oriented
programming. In ECOOP, chapter 10, pages 220–242. 1997.
[30] J. Laird. A fully abstract game semantics of local exceptions. In Logicin Computer Science, Washington, DC, USA, 2001.
[31] Blume Matthias and David McAllester. Sound and complete modelsof contracts. J. Funct. Program., 16:375–414, July 2006.
[32] K McFarlane. Design by contract framework.
[33] Patrick O’Neil Meredith, Dongyun Jin, Dennis Griffith, Feng Chen,and Grigore Roşu. An overview of the MOP runtime verification
framework. International Journal on Software Techniques forTechnology Transfer, 2011. to appear.
[34] B. Meyer. Object-oriented Software Construction. Prentice-Hall,
1988.
[35] B. Meyer. Design by contract. In Advances in Object-Oriented
Software Engineering, pages 1–50. Prentice-Hall, 1991.
[36] B. Meyer. Eiffel: The Language. Prentice-Hall, 1992.
[37] Mark Samuel Miller. Robust composition: towards a unified approachto access control and concurrency control. PhD thesis, Johns Hopkins
University, Baltimore, MD, USA, 2006.
[38] Scott Owens, John Reppy, and Aaron Turon. Regular-expression
derivatives re-examined. J. Funct. Program., 19:173–190, March
2009.
[39] Chris Allan Pavel, Chris Allan, Pavel Avgustinov, Aske Simon
Christensen, Laurie Hendren, Sascha Kuzins, Oege De Moor, Damien
Sereni, Ganesh Sittampalam, and Julian Tibble. Adding trace
matching with free variables to AspectJ. In OOPSLA, pages 345–
364. ACM Press, 2005.
[40] Amir Pnueli. The temporal logic of programs. In Foundations ofComputer Science, pages 46–57, 1977.
[41] John C. Reynolds. The essence of ALGOL, pages 67–88. Birkhauser
Boston Inc., Cambridge, MA, USA, 1997.
[42] David S. Rosenblum. A practical approach to programming withassertions. IEEE Transactions on Software Engineering, 21, 1995.

[17] Matthias Felleisen and Daniel P. Friedman. A calculus for assignments
in higher-order languages. In POPL, pages 314–325, 1987.

[43] Jesse Tov and Riccardo Pucella. Stateful contracts for affine types.
Programming Languages and Systems, pages 550–569, 2010.

[18] R. Findler and M. Felleisen. Contracts for higher-order functions. In
ICFP, 2002.

[44] T. Tuglular, C. A. Muftuoglu, F. Belli, and M. Linschulte. Eventbased input validation using design-by-contract patterns. In Software
Reliability Engineering, pages 195–204, 2009.

[19] Robert Findler and Matthias Blume. Contracts as pairs of projections.
Functional and Logic Programming, pages 226–241, 2006.
[20] Robert Bruce Findler, Matthias Blume, and Matthias Felleisen. An
investigation of contracts as projections. Technical report, Universityof Chicago, 2004.

[45] Dana N. Xu, Simon L. Peyton Jones, and Koen Claessen. Static
contract checking for Haskell. In POPL, pages 41–52, 2009.