TR-2004-02
An Investigation of Contracts as Projections
Robert Bruce Findler; Matthias Blume; Matthias Felleisen. 1 April, 2004.
Communicated by Robby Findler.
Abstract
Software contracts help programmers enforce program properties that the language's type system cannot express. Unlike types, contracts are (usually) enforced at run-time. When a contract fails, the contract system signals an error. Beyond such errors, contracts should have no other observable (functional) effect on the program's results. In most implementations, however, the language of contracts is the full-fledged programming language, which means that programmers may (intentionally or unintentionally) introduce visible effects into their contracts.Here we present the results of investigating the nature of contracts from a denotational perspective. Specifically, we use SPCF and the category of observably sequential functions to show that contracts are best understood as projections. Thus far, the investigation has produced a significantly faster contract implementation and the insight that our contract language cannot express all projections, which in turn has produced a new contract combinator.
Original Document
The original document is available in PDF (uploaded 1 April, 2004 by Robby Findler).
Additional Document Formats
The document is also available in Postscript (uploaded 1 April, 2004 by Robby Findler).
NOTE: The author warrants that these additional documents are identical with the originial to the extent permitted by the translation between the various formats. However, the webmaster has made no effort to verify this claim. If the authenticity of the document is an issue, please always refer to the "Original document." If you find significant alterations, please report to webmaster@cs.uchicago.edu.