A sound (and complete) model of contracts
M. Blume, David McAllester · ACM SIGPLAN Notices · 2004
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 contract-checking 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 avoided by changing the language, replacing unrestricted predicate contracts with a restricted version. The corresponding loss in expressive power can be recovered by also providing a way of explicitly expressing safety as a contract-either in ad-hoc fashion or, e.g., by including general recursive contracts.