Contract Systems Need Domain-Specific Notations

Eiffel’s contract system assumes that programmers can formulate Boolean expressions to articulate simple pre-conditions and post-conditions for methods [33, 34]. Such expressions suffice to state constraints that quotidian type systems cannot express. Here is an example, from Eiffel’s documentation, of a method that sets the seconds field of a clock object:

By monitoring the pre-condition, Eiffel’s contract system can signal an error when control enters the method, not after seconds has been set and retrieved elsewhere. Eiffel’s syntax has require and ensure keywords that cleanly separate specifications from implementations.

Findler and Felleisen [16] generalize Eiffel’s design to modern, higher-order languages with first-class functions and objects. They realize that such a generalization necessitates creating wrappers around behavioral values. Here is the code for checking that a derivative function takes real-valued functions to real-valued functions:

Programmers should never read, let alone write, such complex code. Contract systems, such as the one found in Racket [14, 19], therefore supply the familiar notation from type systems to eliminate these awkward and repetitive patterns:

In other words, developers may use the -> notation as a shorthand for the tedious wrappers in the first version. In Eiffel, contract-specific notations are mere conveniences, but here the notation is essential – writing complex higher-order contracts without them is infeasible.

Moy and Felleisen [37] present an extension of higher-order contracts, dubbed trace contracts, that can express and monitor properties across multiple function and method calls. The idea looks straightforward: collect a trace of method-call events and check the trace with a functional predicate whenever it is updated.

Consider the HasNext property that Java programmers must respect when they use an iterator: each call to next must follow a call to hasNext [39]. A typical implementation would equip the class with an extra field to determine whether a violation has occurred:

Comingling run-time checks with proper functionality in this way is a technique known as defensive programming. As Meyer [33, 34] argued long ago, comingling is bad for the person who maintains the implementation, bad for the person who programs to the interface, and bad for the person who wants to implement the interface differently.

By contrast, a contract system brings relief to all three groups. It enables the developer of an interface to state contracts for cross-cutting specifications and attach them to concrete implementations. A contract, independent of any particular implementation, confers two critical advantages:

1. 1.

   Developers can program to interfaces that express constraints explicitly as code.

2. 2.

   Contracts are compiled to run-time checks that monitor implementations of interfaces, so developers can trust that specification violations are reported in a timely fashion.

With trace contracts, the creator of an iterator class can express the HasNext property as a contract and gain all the benefits thereof. Figure 1 shows a module that exports an iterator object and, in doing so, attaches a contract that concisely states the HasNext property with the regular expression ${(\text{hasNext},\text{next}\mathrm{?})}^{\ast }$ over the alphabet of method names. Other than the usual fully parenthesized syntax of Racket, the regular expression is rendered directly. The use of a problem-specific notation, here regular expressions, clarifies the developer’s intent much better than comingled code, and permits the automated construction of dynamic checks. Each method, after the signature given by ->m, is associated with an event. An event is a value to be added to the trace when that method is called. Here, the events are just atomic symbols: 'has-next and 'next.

Which brings us to a brave new idea: contract systems should be abstracted over domain-specific notations for specifications. In other words, it should be easy to plug in any number of domain-specific specification languages into a contract system. This paper illustrates the idea with trace contracts as the enforcement mechanism and a variety of domain-specific specification languages, which together yield domain-specific contracts (DSCs). The remainder of the paper describes DSCs and the underlying architecture in detail, shows how it works with a simple example (Section 2), presents a more sophisticated example from a real-world API (Section 3), describes a general plan for implementing DSCs in different host languages (Section 4), and evaluates a Racket implementation of DSCs (Section 5).

Many interface specifications employ temporal terminology to constrain sequences of method calls. Consider the MapIterator property from Java’s API [40]. This property states that an Iterator, created from a Collection, which is itself derived from a Map, cannot be used after the Map has been mutated. The word “after” suggests a temporal relationship – a need to look back at whether a mutating method of Map has previously been called.

An interface, therefore, should use a matching formal language, such as temporal logic, to state the property. Given that such statements tend to look at past events, Past-Time Linear Temporal Logic (PLTL) [31] is one suitable choice for stating the MapIterator contract. Indeed, the definition of satisfaction for PLTL formulas employs finite traces of past events – just like trace contracts.

PLTL comes with the primitive temporal operators $\bullet \varphi$ (pronounced “previous”) and $\varphi \text{S}\psi$ (pronounced “since”). Otherwise, PLTL looks like first-order logic. All other temporal operators, for example $◆\varphi$ (pronounced “once”), are derived notions. With these operators, an invalid sequence of method-call events is easy to express: $\text{next}\wedge ◆\text{mutate}.$ In prose, calling the next method of an iterator is invalid if the map has been mutated.

One contribution of this paper is a number of libraries, including one for PLTL, that developers can use in contracts. So, suppose a developer wishes to release a collections library that states and enforces the MapIterator property. Realizing this desire calls for three steps.

First, the developer imports the trace contract library and the PLTL library:

Importing trace-contract brings in, among other forms, object-trace/c. As the introduction mentions, object-trace/c constructs an object contract that records a trace of method-call events. This trace is checked by a predicate every time a new element is added.

Second, the developer formulates and names the PLTL formula associated with the MapIterator property:

Using the PLTL library, a developer can formulate the predicate as the above temporal formula, matching the informal prose found in Java’s documentation. To use a named PLTL formula, a programmer must use the pltl form, which translates it to a (state) machine representation. A machine acts as a predicate over traces, i.e., it can check whether a trace satisfies or refutes a formula:

Third, the developer combines a PLTL expression with object-trace/c to create an enforceable contract. Figure 2 shows a first attempt at such a contract for MapIterator.

As is, these contracts are not quite right. An object-trace/c contract knows only about method calls for the current object. Therefore, map-iterator/c sees only calls to the next method and is unaware of any mutations to the underlying map.

Figure 3 shows how to adapt these contracts to inform the map-iterator/c contract of the other relevant method calls. To express this relationship, the contracts for collection and iterator objects become functions that accept the map/c contract itself. The object-trace/c form uses the keyword this-contract which, similar to this for objects, refers to the object-trace/c contract itself. While the map-collection/c function just passes this contract through to the map-iterator/c function, the latter actually makes use of it. The #:include clause informs the contract system that events from the trace for map/c are to be injected into the trace for map-iterator/c. Consequently, map-iterator-violation, which refers to the 'mutate event, now works correctly in the #:refutes clause.

These contracts look simple, but the underlying property is sophisticated. Consider the scenario where an iterator is created, the underlying map is mutated, and then another iterator is created. It should be the case that the first iterator is invalidated, while the second one is usable. In other words, these two iterators require independent pieces of state. Some events, such as mutations to the underlying map, are shared with both. Other events, such as calls to next, are particular to a specific iterator and are not shared. All this careful state management is handled automatically.

Conversely, manually constructing defensive checks to correctly keep track of this information is difficult. Appendix A shows an implementation of defensive checks for MapIterator, similar to the defensive code shown in Section 1. The code is complex and takes several pages to explain. By contrast, Figure 3 is nearly self-explanatory.

Interfaces should be expressed as directly as possible, using the notation most appropriate for the property at hand. Sometimes a single interface benefits from mixing several domain-specific notations. The DSCs presented in this paper are flexible enough to allow a heterogeneous mixture of notations because they all compile to the same uniform mechanism for capturing and checking traces of events.

This section presents a series of contracts that ensure TCP sockets are used correctly. Consider an idealized TCP interface, similar to the one found in Java, which consists of four classes: a TCP manager, a TCP listener, an input stream, and an output stream. A TCP manager, when given a port number, is responsible for creating a TCP listener that deals with the given port. The purpose of a TCP listener is to accept client connections. For each connected client, a TCP listener produces an input and output stream for receiving and sending data, respectively.

Many languages, including Java, guarantee the following properties of TCP sockets:

• $\mathrm{■}$

  StreamClose. Input and output streams can be used until either the stream itself is closed or the underlying TCP listener is closed.

• $\mathrm{■}$

  PortExclusivity. At any point in the program, there can be at most one active TCP listener on each port.

The Java standard library uses defensive programming to enforce these properties.

Instead, DSCs can nicely express both properties, but they warrant two different notations. The StreamClose property can be expressed as a regular expression:

This regular expression accepts traces of method-call events that use a stream (input or output) until it has been closed, or the underlying listener is closed. There is one unusual feature here, which is the close listener event. In all prior examples, events were symbolic names of methods carrying no additional data. The close listener event also carries the port number of the corresponding listener, which is simply ignored in port-re using a wildcard pattern. Why the close listener event carries a port number will be clarified momentarily.

The PortExclusivity property is not easily expressed as a regular expression. Another formalism, known as quantified event automata (QEA [4]), is a good match:

A QEA is similar to an ordinary finite-state automaton, but it is enriched with quantifiers. By quantifying over a variable, a QEA describes a family of automata: one per instantiation of all quantified variables. Intuitively, manager-qea constructs a two-state automaton for every possible port number. These automata are created on demand, though, to avoid unnecessary overhead. Each automaton starts in the ready state and transitions to the listening state when a new TCP listener is created on that port. When the listener is closed, the automaton moves back to the ready state. Each listener event must carry a port number so the event can be dispatched to the appropriate automaton.

Using object-trace/c, these logical specifications can be connected to the TCP interface itself; see Figure 4. Two differences from the example in Figure 3 are worth pointing out.

First, tcp-manager/c uses the dependent method contract form ->dm [48] to produce an event that is dependent on the argument given to listen. This form permits naming the arguments and result, binding those names for use in the event constructor. Here, the listen event contains the port argument.

Second, tcp-listener/c uses #:extend to contribute events to the parent manager/c contract. As shown in Figure 3, #:include allows events to flow from “ancestor” to “descendant” object. By contrast, the #:extend keyword allows events to flow in the other direction, from “descendant” to “ancestor” object. Specifically, the TCP manager (i.e., the parent) must be aware if a TCP listener (i.e., the child) is closed on a particular port, because then that port becomes available for listening once again according to PortExclusivity. Using #:extendmanager/c tells the contract to communicate close listener events from the listener to the manager. It turns out that StreamClose requires information to flow in the other direction because input and output streams (i.e., the children) must be closed if the underlying listener (i.e., the parent) is closed. This direction is covered using #:include listener/c. In sum, this example demonstrates that object-trace/c can accommodate information flow in both directions, even within the same interface, and can mix distinct notations to check all desired properties.

Implementing DSCs demands two ingredients: a low-level contract system and a mechanism for embedding domain-specific syntax. If a language lacks such a mechanism, a developer can use design patterns to construct embedded languages [41].

Figure 5 graphically summarizes how DSCs work. Each component is combined with a logical formulas (the gray frame). The component’s developers choose the most appropriate logic to use, based on the property to be enforced. These logic languages come with translators that turn these specifications into predicates, which then become pieces of trace contracts. In the diagram, the enforcement mechanism comes into play with the sequences of values that components exchange. The contract code checks the sequence of values that a component receives and sends out. Gray borders on values in Figure 5 indicate that values may acquire a proxy layer that contains specification-checking code from the component’s interface [16, 50]. A proxy interposes on interactions with the underlying object, e.g., a method call, and performs dynamic checks.

This section starts with a brief tutorial of Racket contracts, focusing on trace contracts (Section 4.1). Next, the section introduces essential features of Racket’s domain-specific language (DSL) implementation system (Section 4.2) and what features readers should watch out for when implementing DSCs (Section 4.3). Lastly, the section gives some hints concerning the adaptation of this blueprint to languages with different DSL-programming facilities and contract systems (Section 4.4).

An assessment of the DSC idea and its instantiation with trace contracts must address several aspects: (1) whether DSCs can accommodate existing logic notations; (2) what developer-facing features these implementations provide; and (3) how precisely DSCs can report specification violations. The first two points call for identifying and implementing a corpus of logic notations for specifications in the literature (Section 5.1) and for a qualitative assessment of them along several dimensions (Section 5.2). The last point is a matter of implementation quality; an extensive test suite can validate that the blame assignment points to the problematic party for some common example properties from the literature (Section 5.3). In addition, this section relates the DSC idea to prior work (Section 5.4).

Racket makes it straightforward to instantiate the DSC idea. It comes with an expressive library of contract combinators and a powerful facility for creating domain-specific notations. Leveraging the latter allows the creators of DSCs to implement notations with little effort and translate them to contract expressions. End-users can employ a library that provides DSCs just like any other dependency – critically, while continuing to use, and benefiting from, existing IDEs.

While the Racket implementation is particularly straightforward, several programming languages offer similar combinations of metaprogramming and contract features. For example, Clojure has ported most of Racket’s contract system and comes with its own macro system. Scala too has a rich metaprogramming system for embedding DSLs [44] and could be equipped with a contract system based on Java’s assertion system.

This paper has discussed the DSC idea only in the context of trace contracts with temporal specification languages. However, the idea of combining contracts with domain-specific specification languages goes far beyond that particular instantiation. For example, effect-handler contracts [36] combined with an authorization logic [1] yields authorization contracts [35] that can enforce security properties. Or, network-aware contracts [52] combined with a DSL for describing the legal moves of a game [12] yields the rule checker for an implementation of an online game. Indeed, there are plenty of other combinations not yet studied and worthy of exploration from the DSC perspective. Contracts and DSLs are useful alone. But together, they are better.