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...

• Type: Conference
• Year: 2004
• Where: ICFP
• Authors: Matthias Blume, David A. McAllester
• Keywords: General Recursive Contracts, ICFP 2004, Original Unrestricted Predicate, Programming Languages, Unrestricted Predicate Contracts