A sound (and complete) model of contracts

10 years 1 months ago
A sound (and complete) model of contracts
Even in statically typed languages it is useful to have certain invariants checked dynamically. Findler and Felleisen gave an algorithm for dynamically checking expressive higher-order types called contracts. If we postulate soundness (in the sense that whenever a term is accused of violating its contract it really does fail to satisfy it), then their algorithm implies a semantics for contracts. Unfortunately, the implicit nature of the resulting model makes it rather unwieldy. In this paper we demonstrate that a direct approach yields essentially the same semantics without having to refer to contractchecking in its definition. The so-defined model largely coincides with intuition, but it does expose some peculiarities in its interpretation of predicate contracts where a notion of safety (which we define in the paper) "leaks" into the semantics of Findler and Felleisen's original unrestricted predicate contracts. This counter-intuitive aspect of the semantics can be avo...
Matthias Blume, David A. McAllester
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2004
Where ICFP
Authors Matthias Blume, David A. McAllester
Comments (0)