A sound (and complete) model of contracts

ABSTRACT

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.

REFERENCES

• 1: Andrew W. Appel , David McAllester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.657-683, September 2001 [doi>10.1145/504709.504712]
• 2: Kim B. Bruce , Luca Cardelli , Benjamin C. Pierce, Comparing Object Encodings, Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, p.415-438, September 23-26, 1997
• 3: T. H. Brus , C. J. D. van Eekelen , M. O. van Leer , M. J. Plasmeijer, CLEAN: A language for functional graph rewriting, Proc. of a conference on Functional programming languages and computer architecture, p.364-384, October 1987, Portland, Oregon, United States
• 4: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 5: M. Felleisen , R. B. Findler , M. Flatt , S. Krishnamurthi, The DrScheme project: an overview, ACM SIGPLAN Notices, v.33 n.6, p.17-23, June 1998 [doi>10.1145/284563.284566]
• 6: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 7: R. B. Findler, M. Blume, and M. Felleisen. An investigation of contracts as projections. Technical Report TR-2004-02, University of Chicago Computer Science Department, 2004.
• 8: Robert Bruce Findler , John Clements , Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Paul Steckler , Matthias Felleisen, DrScheme: a programming environment for Scheme, Journal of Functional Programming, v.12 n.2, p.159-182, March 2002 [doi>10.1017/S0956796801004208]
• 9: Robert Bruce Findler , Matthias Felleisen, Contracts for higher-order functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.48-59, October 04-06, 2002, Pittsburgh, PA, USA
• 10: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 11: S. P. Jones. Haskell 98 Language and Libraries. Cambridge University Press, 2003.
• 12: X. Leroy. The ZINC experiment: an economical implementation of the ML language. Technical Report No. 117, INRIA, Feb. 1990.
• 13: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 14: H. G. Rice. Classes of recursively enumerable sets and their decision problems. Trans. Amer. Math. Soc., 74:358--366, 1953.
• 15: D. S. Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97--136. Springer, 1972.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

General Terms:
Languages, Theory, Verification

Keywords:
contracts, predicates, safety