research-article

ICFP 2002: Contracts for higher-order functions

Authors:

Robert Bruce Findler,

Matthias FelleisenAuthors Info & Claims

ACM SIGPLAN Notices, Volume 48, Issue 4S

Pages 34 - 45

https://doi.org/10.1145/2502508.2502521

Published: 09 July 2013 Publication History

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 Dr Scheme. We establish basic properties of the model (type soundness, etc.) and illustrate the usefulness of contract checking with examples from Dr Scheme's code base.

We believe that the development of an assertion system for higherorder 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. nOn 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]

Clinger, W. D. Proper tail recursion and space efficiency. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 174--185, June 1998.

Digital Library

[3]

Felleisen, M., R. B. Findler, M. Flatt and S. Krishnamurthi. How to Design Programs. MIT Press, 2001.

[4]

Felleisen, M. and R. Hieb. The revised report on the syntactic theories of sequential control and state. In Theoretical Computer Science, pages 235--271, 1992.

Digital Library

[5]

Findler, R. B., J. Clements, C. Flanagan, M. Flatt, S. Krishnamurthi, P. Steckler and M. Felleisen. DrScheme: A programming environment for Scheme. Journal of Functional Programming, 12(2):159--182, March 2002. A preliminary version of this paper appeared in PLILP 1997, LNCS volume 1292, pages 369--388.

Digital Library

[6]

Findler, R. B. and M. Felleisen. Contracts for higher-order functions. Technical Report NU-CCS-02-05, Northeastern University, 2002.

Digital Library

[7]

Findler, R. B. and M. Flatt. Modular object-oriented programming with units and mixins. In Proceedings of ACM SIGPLAN International Conference on Functional Programming, pages 94--104, September 1998.

Digital Library

[8]

Flatt, M. PLT MzScheme: Language manual. Technical Report TR97-280, Rice University, 1997. http://www.pltscheme. org/software/mzscheme/.

[9]

Flatt, M. Composable and compilable macros: You want it when? In Proceedings of ACM SIGPLAN International Conference on Functional Programming, 2002.

Digital Library

[10]

Flatt, M., S. Krishnamurthi and M. Felleisen. A programmer's reduction semantics for classes and mixins. Formal Syntax and Semantics of Java, 1523:241--269, 1999. Preliminary version appeared in proceedings of Principles of Programming Languages, 1998. Revised version is Rice University technical report TR 97-293, June 1999.

Digital Library

[11]

Gomes, B., D. Stoutamire, B. Vaysman and H. Klawitter. A Language Manual for Sather 1.1, August 1996.

[12]

Gosling, J., B. Joy and J. Guy Steele. The Java¿ Language Specification. Addison-Wesley, 1996.

Digital Library

[13]

Harper, R. and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Proceedings of ACM Conference Principles of Programming Languages, pages 123--137, Janurary 1994.

Digital Library

[14]

Holt, R. C. and J. R. Cordy. The Turing programming language. In Communications of the ACM, volume 31, pages 1310--1423, December 1988.

Digital Library

[15]

Jones, M. P., A. Reid and The Yale Haskell Group. The Hugs 98 User Manual, 1999.

[16]

Kelsey, R., W. Clinger and J. R. (Editors). Revised5 report of the algorithmic language Scheme. ACM SIGPLAN Notices, 33(9):26--76, 1998.

Digital Library

[17]

Kölling, M. and J. Rosenberg. Blue: Language Specification, version 0.94, 1997.

[18]

Leroy, X. Manifest types, modules, and separate compilation. In Proceedings of ACM Conference Principles of Programming Languages, pages 109--122, Janurary 1994.

Digital Library

[19]

Leroy, X. The Objective Caml system, Documentation and User's guide, 1997.

[20]

Luckham, D. Programming with specifications. Texts and Monographs in Computer Science, 1990.

Digital Library

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

Digital Library

[22]

Meyer, B. Eiffel: The Language. Prentice Hall, 1992.

Digital Library

[23]

Milner, R., M. Tofte and R. Harper. The Definition of Standard ML. MIT Press, 1990.

Digital Library

[24]

Mitchell, J. C. and G. D. Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470--502, 1988.

Digital Library

[25]

Parnas, D. L. A technique for software module specification with examples. Communications of the ACM, 15(5):330--336, May 1972.

Digital Library

[26]

Rémy, D. and J. Vouillon. Objective ML: A simple objectoriented extension of ML. In Proceedings of ACM Conference Principles of Programming Languages, pages 40--53, January 1997.

Digital Library

[27]

Rosenblum, D. S. A practical approach to programming with assertions. IEEE Transactions on Software Engineering, 21(1):19--31, Janurary 1995.

Digital Library

[28]

Serrano, M. Bigloo: A practical Scheme compiler, 1992--2002.

[29]

Serrano, M. Bee: an integrated development environment for the Scheme programming language. Journal of Functional Programming, 10(2):1--43, May 2000.

Digital Library

[30]

Steele, G. L. J. Debunking the "expensive procedure call" myth; or, Procedure call implementations considered harmful; or, LAMBDA: The ultimate goto. Technical Report 443, MIT Artificial Intelligence Laboratory, 1977. First appeared in the Proceedings of the ACM National Conference (Seattle, October 1977), 153--162.

Digital Library

[31]

Switzer, R. Eiffel: An Introduction. Prentice Hall, 1993.

Digital Library

[32]

Szyperski, C. Component Software. Addison-Wesley, 1998.

[33]

The GHC Team. The Glasgow Haskell Compiler User's Guide, 1999.

[34]

Wright, A. and M. Felleisen. A syntactic approach to type soundness. Information and Computation, pages 38--94, 1994. First appeared as Technical Report TR160, Rice University, 1991.

Digital Library

Cited By

Chen TSiek J(2024)Quest Complete: The Holy Grail of Gradual SecurityProceedings of the ACM on Programming Languages10.1145/36564428:PLDI(1609-1632)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656442
Hoeflich JFindler RSerrano M(2022)Highly illogical, Kirk: spotting type mismatches in the large despite broken contracts, unsound types, and too many lintersProceedings of the ACM on Programming Languages10.1145/35633056:OOPSLA2(479-504)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563305
Wolff FBílý AMatheja CMüller PSummers A(2021)Modular specification and verification of closures in RustProceedings of the ACM on Programming Languages10.1145/34855225:OOPSLA(1-29)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485522

Index Terms

ICFP 2002: Contracts for higher-order functions
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
  2. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

Contracts for higher-order functions
ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming

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 ...
Contracts for higher-order functions

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 ...
Future contracts
PPDP '09: Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming

Many recent research projects focus on language support for behavioral software contracts, that is, assertions that govern the boundaries between software building blocks such as procedures, classes, or modules. Contracts primarily help locate bugs in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 48, Issue 4S

Supplemental issue

April 2013

71 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2502508

Issue’s Table of Contents

Copyright © 2013 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 July 2013

Published in SIGPLAN Volume 48, Issue 4S

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
103
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chen TSiek J(2024)Quest Complete: The Holy Grail of Gradual SecurityProceedings of the ACM on Programming Languages10.1145/36564428:PLDI(1609-1632)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656442
Hoeflich JFindler RSerrano M(2022)Highly illogical, Kirk: spotting type mismatches in the large despite broken contracts, unsound types, and too many lintersProceedings of the ACM on Programming Languages10.1145/35633056:OOPSLA2(479-504)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563305
Wolff FBílý AMatheja CMüller PSummers A(2021)Modular specification and verification of closures in RustProceedings of the ACM on Programming Languages10.1145/34855225:OOPSLA(1-29)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485522

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents