Contracts for higher-order functions

ABSTRACT

Assertions play an important role in the construction of robust software. Their use in programming languages dates back to the 1970s. Eiffel, an object-oriented programming language, wholeheartedly adopted assertions and developed the "Design by Contract" philosophy. Indeed, the entire object-oriented community recognizes the value of assertion-based contracts on methods.In contrast, languages with higher-order functions do not support assertion-based contracts. Because predicates on functions are, in general, undecidable, specifying such predicates appears to be meaningless. Instead, the functional languages community developed type systems that statically approximate interesting predicates.In this paper, we show how to support higher-order function contracts in a theoretically well-founded and practically viable manner. Specifically, we introduce λ^con, a typed lambda calculus with assertions for higher-order functions. The calculus models the assertion monitoring system that we employ in DrScheme. We establish basic properties of the model (type soundness, etc.) and illustrate the usefulness of contract checking with examples from DrScheme's code base.We believe that the development of an assertion system for higher-order functions serves two purposes. On one hand, the system has strong practical potential because existing type systems simply cannot express many assertions that programmers would like to state. On the other hand, an inspection of a large base of invariants may provide inspiration for the direction of practical future type system research.

REFERENCES

• 1: AT&T Bell Labratories. Standard ML of New Jersey, 1993.
• 2: William D. Clinger, Proper tail recursion and space efficiency, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.174-185, June 17-19, 1998, Montreal, Quebec, Canada
• 3: Felleisen, M., R. B. Findler, M. Flatt and S. Krishnamurthi. How to Design Programs. MIT Press, 2001.
• 4: 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]
• 5: Robert Bruce Findler , Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, DrScheme: A Pedagogic Programming Environment for Scheme, Proceedings of the9th International Symposium on Programming Languages: Implementations, Logics, and Programs: Including a Special Trach on Declarative Programming Languages in Education, p.369-388, September 03-05, 1997
• 6: Findler, R. B. and M. Felleisen. Contracts for higher-order functions. Technical Report NU-CCS-02-05, Northeastern University, 2002.
• 7: Robert Bruce Findler , Matthew Flatt, Modular object-oriented programming with units and mixins, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.94-104, September 26-29, 1998, Baltimore, Maryland, United States
• 8: Flatt, M. PLT MzScheme: Language manual. Technical Report TR97-280, Rice University, 1997. http://www.plt-scheme.org/software/mzscheme/.
• 9: Matthew Flatt, Composable and compilable macros:: you want it when?, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.72-83, October 04-06, 2002, Pittsburgh, PA, USA
• 10: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, A Programmer's Reduction Semantics for Classes and Mixins, Formal Syntax and Semantics of Java, p.241-269, January 1999
• 11: Gomes, B., D. Stoutamire, B. Vaysman and H. Klawitter. A Language Manual for Sather 1.1, August 1996.
• 12: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 13: Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
• 14: Richard C. Holt , James R. Cordy, The Turing programming language, Communications of the ACM, v.31 n.12, p.1410-1423, Dec. 1988 [doi>10.1145/53580.53581]
• 15: Jones, M. P., A. Reid and The Yale Haskell Group. The Hugs 98 User Manual, 1999.
• 16: N. I. Adams, IV , D. H. Bartley , G. Brooks , R. K. Dybvig , D. P. Friedman , R. Halstead , C. Hanson , C. T. Haynes , E. Kohlbecker , D. Oxley , K. M. Pitman , G. J. Rozas , G. L. Steele, Jr. , G. J. Sussman , M. Wand , H. Abelson, Revised5 report on the algorithmic language scheme, ACM SIGPLAN Notices, v.33 n.9, p.26-76, Sept. 1, 1998 [doi>10.1145/290229.290234]
• 17: Kölling, M. and J. Rosenberg. Blue: Language Specification, version 0.94, 1997.
• 18: Xavier Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-122, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176926]
• 19: Leroy, X. The Objective Caml system, Documentation and User's guide, 1997.
• 20: David C. Luckham, Programming with Specifications: An Introduction to Anna, a Language for Specifying ADA Programs, Springer-Verlag New York, Inc., Secaucus, NJ, 1990
• 21: Luckham, D. C. and F. von Henke. An overview of Anna, a specification language for Ada. In IEEE Software, volume 2, pages 9--23, March 1985.
• 22: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 23: Robin Milner , Mads Tofte , Robert Harper, The Definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 24: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 25: D. L. Parnas, A technique for software module specification with examples, Communications of the ACM, v.15 n.5, p.330-336, May 1972 [doi>10.1145/355602.361309]
• 26: Didier Rémy , Jérôme Vouillon, Objective ML: a simple object-oriented extension of ML, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.40-53, January 15-17, 1997, Paris, France [doi>10.1145/263699.263707]
• 27: David S. Rosenblum, A Practical Approach to Programming With Assertions, IEEE Transactions on Software Engineering, v.21 n.1, p.19-31, January 1995 [doi>10.1109/32.341844]
• 28: Serrano, M. Bigloo: A practical Scheme compiler, 1992--2002.
• 29: Manuel Serrano, Bee: an integrated development environment for the Scheme programming language, Journal of Functional Programming, v.10 n.4, p.353-395, July 2000 [doi>10.1017/S0956796800003725]
• 30: Guy Lewis Steele, Jr., Debunking the “expensive procedure call” myth or, procedure call implementations considered harmful or, LAMBDA: The Ultimate GOTO, Proceedings of the 1977 annual conference, p.153-162, January 1977 [doi>10.1145/800179.810196]
• 31: Robert Switzer, Eiffel: an introduction, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 32: Szyperski, C. Component Software. Addison-Wesley, 1998.
• 33: The GHC Team. The Glasgow Haskell Compiler User's Guide, 1999.
• 34: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

General Terms:
Design, Languages, Reliability

Keywords:
behavioral specifications, contracts, higher-order functions, predicate typing, solfware reliability