article

Oh Lord, please don't let contracts be misunderstood (functional pearl)

Authors:

Christos Dimoulas,

Robert Bruce Findler,

Matthias FelleisenAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 9

Pages 117 - 131

https://doi.org/10.1145/3022670.2951930

Published: 04 September 2016 Publication History

Abstract

Contracts feel misunderstood, especially those with a higher-order soul. While software engineers appreciate contracts as tools for articulating the interface between components, functional programmers desperately search for their types and meaning, completely forgetting about their pragmatics.

This gem presents a novel analysis of contract systems. Applied to the higher-order kind, this analysis reveals their large and clearly unappreciated software engineering potential. Three sample applications illustrate where this kind of exploration may lead.

References

[1]

Parker Abercrombie and Murat Karaorman. jContractor: Bytecode Instrumentation Techniques for Implementing Design by Contract in Java. Electronic Notes in Theoretical Computer Science (70(4)), pp. 55–79, 2002. Presented in RV 2001, Run-time Verification (Satellite Workshop of FLoC '02)

[2]

Chris Allan, Pavel Avgustinov, Aske Simon Christensen, Laurie Hendren, Sacha Kuzins, Ondˇrej Lhoták, Oege de Moor, Damien Sereni, Ganesh Sittampalam, and Julian Tibble. Adding Trace Matching with Free Variables to AspectJ. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pp. 345–364, 2005.

Digital Library

[3]

Pavel Avgustinov, Julian Tibble, and Oege de Moor. Making Trace Monitors Feasible. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pp. 589–608, 2007.

Digital Library

[4]

Howard Barringer, David Rydeheard, and Klaus Havelund. Rule Systems for Run-time Monitoring: From Eagle to Ruler. In Proc. International Conference on Runtime Verification, pp. 111–125, 2007.

Digital Library

[5]

Detlef Bartetzko, Clemens Fischer, Michael Möller, and Heike Wehrheim. Jass — Java with Assertions. Electronic Notes in Theoretical Computer Science (55(2)), pp. 103–117, 2001. Presented in RV 2001, Run-time Verification (Satellite Workshop of CAV '01)

[6]

Antoine Beugnard, Jean-Marc Jézéquel, Noël Plouzeau, and Damien Watkins. Contract Aware Components, 10 years after. Electronic Proceedings in Theoretical Computer Science (7), pp. 1–11, 2010.

[7]

Matthias Blume and David McAllester. Sound and Complete Models of Contracts. Journal of Functional Programming 16(4-5), pp. 367–414, 2006.

Digital Library

[8]

Eric Bodden. J-LO, a Tool for Runtime-Checking Temporal Assertions. RWTH Aachen University, 2005. Master's Thesis.

[9]

Feng Chen and Grigore Ro¸su. Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation. Electronic Notes in Theoretical Computer Science (89(2)), pp. 108–127, 2003. Presented in RV 2003, Runtime Verification (Satellite Workshop of CAV '03)

[10]

Thierry Coquand and Gerard Huet. The Calculus of Constructions. Information and Compuation(76:2-3), pp. 95–120, 1988.

Digital Library

[11]

Ryan Culpeppeer. Fortifying Macros. Journal of Functional Programming (22(4/5)), pp. 439–476, 2012.

Digital Library

[12]

Ryan Culpeppeer and Matthias Felleisen. Fortifying Macros. In Proc. ACM International Conference on Functional Programming, pp. 235–246, 2010.

Digital Library

[13]

Christos Dimoulas and Matthias Felleisen. On Contract Satisfaction in a Higher-Order World. Transactions on Programming Languages and Systems 33(5), pp. 16:1–16:29, 2011.

Digital Library

[14]

Christos Dimoulas, Robert Bruce Findler, Cormac Flanagan, and Matthias Felleisen. Correct Blame for Contracts: No More Scapegoating. In Proc. ACM Symposium on Principles of Programming Languages, pp. 215–226, 2011.

Digital Library

[15]

Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Complete Monitors for Behavioral Contracts. In Proc. European Symposium on on Programming, pp. 214– 233, 2012.

Digital Library

[16]

Tim Disney, Cormac Flanagan, and Jay McCarthy. Temporal Higher-order Contracts. In Proc. ACM International Conference on Functional Programming, pp. 176–188, 2011.

Digital Library

[17]

Doron Drusinsky. Temporal Rover. 2010. http://www. time-rover.com

[18]

Matthias Felleisen. On the Expressive Power of Programming Languages. Science of Programming 17, pp. 35–75, 1991.

Digital Library

[19]

Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. MIT Press, 2009.

Digital Library

[20]

Robert Bruce Findler and Matthias Blume. Contracts as Pairs of Projections. In Proc. International Conference on Functional and Logic Programming, pp. 226–241, 2006.

Digital Library

[21]

Robert Bruce Findler, John Clements, Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Paul Steckler, and Matthias Felleisen. DrScheme: a Programming Environment for Scheme. Journal of Functional Programming 12(2), pp. 159–182, 2002.

Digital Library

[22]

Robert Bruce Findler and Matthias Felleisen. Contracts for Higher-Order Functions. In Proc. ACM International Conference on Functional Programming, pp. 48–59, 2002.

Digital Library

[23]

Robert Bruce Findler, Matthias Felleisen, and Matthias Blume. An Investigation of Contracts as Projections. University of Chicago, Computer Science Department, TR-2004-02, 2004.

[24]

Cormac Flanagan. Hybrid Type Checking. In Proc. ACM Symposium on Principles of Programming Languages, pp. 245–256, 2006.

Digital Library

[25]

Matthew Flatt, Eli Barzilay, and Robert Bruce Findler. Scribble: Closing the Book on Ad Hoc Documentation Tools. In Proc. ACM International Conference on Functional Programming, pp. 109–120, 2009.

Digital Library

[26]

Matthew Flatt, Robert Bruce Findler, and Matthias Felleisen. Scheme with Classes, Mixins, and Traits. In Proc. Asian Symposium on Programming Languages and Systems, pp. 270–289, 2006.

Digital Library

[27]

Matthew Flatt and PLT. Reference: Racket. PLT Inc., PLTTR-2010-1, 2010. http://racket-lang.org/tr1/

[28]

Martin Gasbichler and Michael Sperber. Integrating User-Level Threads with Processes in Scsh. Higher Order and Symbolic Computation (18(3-4)), pp. 327–354, 2005.

Digital Library

[29]

Ann Q. Gates, Steve Roach, Oscar Mondragon, and Nelly Delgado. DynaMICs: Comprehensive Support for Run-Time Monitoring. In Proc. International Conference on Runtime Verification, pp. 164–180, 2001.

[30]

Simon F. Goldsmith, Robert O'Callahan, and Alex Aiken. Relational Queries over Program Traces. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pp. 385–402, 2005.

Digital Library

[31]

Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. Contracts Made Manifest. In Proc. ACM Symposium on Principles of Programming Languages, pp. 353–364, 2010.

Digital Library

[32]

Guy Lewis Steele, Jr. Macaroni is Better Than Spaghetti. In Proc. Symposium on Artificial Intelligence and Programming Languages, pp. 60–66, 1977.

Digital Library

[33]

Guy Lewis Steele, Jr. The Revised Report on SCHEME: A Dialect of LISP. Massachusetts Institute of Technology Artificial Intelligence Laboratory, AIM-452, 1978.

[34]

Klaus Havelund and Grigore Ro¸su. Monitoring Java Programs with Java PathExplorer. Electronic Notes in Theoretical Computer Science (55(2)), pp. 200–217, 2001. Presented in RV 2001, Run-time Verification (Satellite Workshop of CAV '01)

[35]

Phillip Heidegger, Annette Bieniusa, and Peter Thiemann. Access Permission Contracts for Scripting Languages. In Proc. ACM Symposium on Principles of Programming Languages, pp. 112–122, 2012.

Digital Library

[36]

Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language Primitives and Type Discipline for Structured Communication-Based Programming. In Proc. European Symposium on on Programming, pp. 122–138, 1998.

Digital Library

[37]

Moonzoo Kim, Mahesh Viswanathan, Sampath Kannan, Insup Lee, and Oleg Sokolsky. Java-MaC: A Run-Time Assurance Approach for Java Programs. Formal Methods in System Design (24(2)), pp. 129–155, 2004.

Digital Library

[38]

John Lamping. Typing the Specialization Interface. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pp. 201–214, 1993.

Digital Library

[39]

Gary T. Leavens. JML’s Rich, Inherited Specifications for Behavioral Subtypes. In Proc. Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods, pp. 2–34, 2006.

Digital Library

[40]

Marcelo D'Amorim and Klaus Havelund. Event-based Runtime Verification of Java Programs. In Proc. Workshop on Dynamic Analysis, pp. 1–7, 2005.

Digital Library

[41]

Michael Martin, Benjamin Livshits, and Monica S. Lam. Finding Application Errors and Security Flaws Using PQL: a Program Query Language. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pp. 365–383, 2005.

Digital Library

[42]

Jay McCarthy. The Two-state Solution: Native and Serializable Continuations Accord. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pp. 567–582, 2010.

Digital Library

[43]

Patrick Meredith and Grigore Ro¸su. Efficient Parametric Runtime Verification with Deterministic String Rewriting. In Proc. ACM/IEEE International Conference on Automated Software Engineering, pp. 70–80, 2013.

[44]

Bernard Meyer. Applying Design by Contract. IEEE Computer 25(10), pp. 45–51, 1992.

Digital Library

[45]

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

Digital Library

[46]

Scott Moore, Christos Dimoulas, Dan King, and Stephen Chong. Shill: A Secure Shell Scripting Language. In Proc. USENIX Symposium on Operating Systems Design and Implementation, pp. 183–199, 2014.

Digital Library

[47]

James Hiram Morris. Lambda-Calculus Models of Programming Languages. Ph.D. dissertation, Massachusetts Institute of Technology, 1968.

[48]

Phúc Nguy˜ên and David Van Horn. Relatively Complete Counterexamples for Higher-order Programs. In Proc. ACM Conference on Programming Language Design and Implementation, pp. 445–456, 2015.

Digital Library

[49]

Phúc Nguy˜ên, Sam Tobin-Hochstadt, and David Van Horn. Soft Contract Verification. In Proc. ACM International Conference on Functional Programming, pp. 139–152, 2014.

Digital Library

[50]

Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. Liquid Types. In Proc. ACM Conference on Programming Language Design and Implementation, pp. 159–169, 2008.

Digital Library

[51]

Christophe Scholliers, Éric Tanter, and Wolfgang De Meuter. Computational Contracts. Science of Computer Programming (98:3), pp. 360–375, 2015.

Digital Library

[52]

Herbert A. Simon. Administrative Behavior. MacMillan, 1947.

[53]

Vincent St-Amour, Leif Andersen, and Matthias Felleisen. Feature-specific Profiling. In Proc. Compiler Construction, pp. 49–68, 2015.

[54]

Robert E. Storm and Shaula A. Yemini. Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Transactions on Software Engineering(12(1)), pp. 157–171, 1986.

Digital Library

[55]

T. Stephen Strickland, Christos Dimoulas, Asumu Takikawa, and Matthias Felleisen. Contracts for First-Class Classes. Transactions on Programming Languages and Systems 35(3), pp. 11:1–1:58, 2013.

Digital Library

[56]

T. Stephen Strickland and Matthias Felleisen. Nested and Dynamic Contract Boundaries. In Proc. International Conference on Functional and Logic Programming, pp. 141–158, 2009.

[57]

T. Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt. Chaperones and Impersonators: Run-time Support for Reasonable Interposition. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pp. 943–962, 2012.

Digital Library

[58]

Asumu Takikawa, T. Stephen Strickland, and Sam Tobin-Hochstadt. Constraining Delimited Control with Contracts. In Proc. European Symposium on on Programming, pp. 229– 248, 2013.

Digital Library

[59]

The Coq Cevelopment Team. The Coq Proof Assistant Reference Manual. LogiCal Project, Version 8.0, 2004.

[60]

Philip Wadler and Robert Bruce Findler. Well-typed Programs Can’t be Blamed. In Proc. European Symposium on on Programming, pp. 1–15, 2009.

Digital Library

Cited By

Bueso de Barrio LFredlund LHerranz ÁMariño JBenac Earle C(2025)Executable contracts for ElixirJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.101019142(101019)Online publication date: Jan-2025
https://doi.org/10.1016/j.jlamp.2024.101019
Felleisen MFindler RFlatt MKrishnamurthi SBarzilay EMcCarthy JTobin-Hochstadt S(2018)A programmable programming languageCommunications of the ACM10.1145/312732361:3(62-71)Online publication date: 21-Feb-2018
https://dl.acm.org/doi/10.1145/3127323
Vandenbogaerde BStiévenart QDe Roover C(2024)Blame-Correct Support for Receiver Properties in Recursively-Structured Actor ContractsProceedings of the ACM on Programming Languages10.1145/36746438:ICFP(515-543)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674643
Show More Cited By

Index Terms

Oh Lord, please don't let contracts be misunderstood (functional pearl)
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

Oh Lord, please don't let contracts be misunderstood (functional pearl)
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Contracts feel misunderstood, especially those with a higher-order soul. While software engineers appreciate contracts as tools for articulating the interface between components, functional programmers desperately search for their types and meaning, ...
Modelling Legal Contracts as Processes
DEXA '00: Proceedings of the 11th International Workshop on Database and Expert Systems Applications

This paper concentrates on the representation of legal relations that occur between parties once they have entered a contractual agreement and their evolution as the agreement progresses through time. Contracts are regarded as processes and they are ...
Subcontracting, Assignment, and Substitution for Legal Contracts in Symboleo
Conceptual Modeling
Abstract
Legal contracts specify obligations and powers among legal subjects, involve assets, and are subject to quality constraints. Smart contracts are software systems that monitor the execution of contracts to ensure compliance. As a starting point for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 9

ICFP '16

September 2016

501 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3022670

Editor:
Matthew Fluet

Issue’s Table of Contents

ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
September 2016
501 pages
ISBN:9781450342193
DOI:10.1145/2951913
General Chairs:
Jacques Garrigue
Nagoya University, Japan
,
Gabriele Keller
University of New South Wales, Australia
,
Program Chair:
Eijiro Sumii
Tohoku University, Japan

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 September 2016

Published in SIGPLAN Volume 51, Issue 9

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
469
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)1

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bueso de Barrio LFredlund LHerranz ÁMariño JBenac Earle C(2025)Executable contracts for ElixirJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.101019142(101019)Online publication date: Jan-2025
https://doi.org/10.1016/j.jlamp.2024.101019
Felleisen MFindler RFlatt MKrishnamurthi SBarzilay EMcCarthy JTobin-Hochstadt S(2018)A programmable programming languageCommunications of the ACM10.1145/312732361:3(62-71)Online publication date: 21-Feb-2018
https://dl.acm.org/doi/10.1145/3127323
Vandenbogaerde BStiévenart QDe Roover C(2024)Blame-Correct Support for Receiver Properties in Recursively-Structured Actor ContractsProceedings of the ACM on Programming Languages10.1145/36746438:ICFP(515-543)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674643
Vandenbogaerde BChristakis MPradel M(2024)Soft Verification for Actor Contract SystemsProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685551(1891-1895)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685551
Moy CDimoulas CFelleisen M(2024)Effectful Software ContractsProceedings of the ACM on Programming Languages10.1145/36329308:POPL(2639-2666)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632930
MOY CFELLEISEN M(2023)Trace contractsJournal of Functional Programming10.1017/S095679682300009633Online publication date: 13-Dec-2023
https://doi.org/10.1017/S0956796823000096
Vandenbogaerde BStievenart QDe Roover C(2022)Summary-Based Compositional Analysis for Soft Contract Verification2022 IEEE 22nd International Working Conference on Source Code Analysis and Manipulation (SCAM)10.1109/SCAM55253.2022.00028(186-196)Online publication date: Oct-2022
https://doi.org/10.1109/SCAM55253.2022.00028
VAN STRYDONCK TPIESSENS FDEVRIESE D(2021)Linear capabilities for fully abstract compilation of separation-logic-verified codeJournal of Functional Programming10.1017/S095679682100002231Online publication date: 30-Mar-2021
https://doi.org/10.1017/S0956796821000022
Lazarek LKing ASundar SFindler RDimoulas C(2019)Does blame shifting work?Proceedings of the ACM on Programming Languages10.1145/33711334:POPL(1-29)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371133
Homer MJones TNoble JMarr SFumero J(2019)First-class dynamic typesProceedings of the 15th ACM SIGPLAN International Symposium on Dynamic Languages10.1145/3359619.3359740(1-14)Online publication date: 20-Oct-2019
https://dl.acm.org/doi/10.1145/3359619.3359740
Show More Cited By

View Options

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