Contracts as Pairs of Projections

Robby Findler; Matthias Blume. 20 January, 2006.
Communicated by Robby Findler.
Supersedes: TR-2005-15 (updated 01/20/06)


Assertion-based contracts provide a powerful mechanism for stating invariants at module boundaries and for enforcing them uniformly. In 2002, Findler and Felleisen showed how to add contracts to higher-order functional languages, allowing programmers to assert invariants about functions as values. Following up in 2004, Blume and McAllester provided a quotient model for contracts. Roughly speaking, their model equates a contract with the set of values that cannot violate the contract. Their studies raised interesting questions about the nature of contracts and, in particular, the nature of the "any" contract.

In this paper, we develop a model for software contracts that follows Dana Scott's program by interpreting contracts as projections. The model has already improved our implementation of contracts. We also demonstrate how it increases our understanding of contract-oriented programming and design. In particular, our work provides a definitive answer to the questions raised by Blume and McAllester's work. The key insight from our model that resolves those questions is that a contract that puts no obligation on either party is not the same as the most permissive contract for just one of the parties.

Original Document

The original document is available in PDF (uploaded 20 January, 2006 by Robby Findler).