A sound (and complete) model of contracts

14 years 4 months ago

Download people.cs.uchicago.edu

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

Real-time Traffic