Document Open Access Logo

Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea)

Authors Cameron Moy , Ryan Jung , Matthias Felleisen

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.42.pdf
  • Filesize: 0.95 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Software and its engineering → Domain specific languages
Keywords
  • software contracts
  • domain-specific languages

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Contract systems enable programmers to state specifications and have them enforced at run time. First-order contracts are expressed using ordinary code, while higher-order contracts are expressed using the notation familiar from type systems. Most interface descriptions, though, come with properties that involve not just assertions about single method calls, but entire call chains. Typical contract systems cannot express these specifications concisely. Such specifications demand domain-specific notations. In response, this paper proposes that contract systems abstract over the notation used for stating specifications. It presents an architecture for such a system, some illustrative examples, and an evaluation in terms of common notations from the literature.

Cite As Get BibTex

Cameron Moy, Ryan Jung, and Matthias Felleisen. Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 42:1-42:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.42

Author Details

Cameron Moy
  • PLT @ Northeastern University, Boston, MA, USA
Ryan Jung
  • Northeastern University, Boston, MA, USA
Matthias Felleisen
  • PLT @ Northeastern University, Boston, MA, USA

Funding

This work was supported by NSF grant SHF 2116372.

Supplementary Materials

References

  1. Owen Arden, Jed Liu, and Andrew C. Myers. Flow-Limited Authorization. In Computer Security Foundations (CSF), 2015. URL: https://doi.org/10.1109/csf.2015.42.
  2. Michael Ballantyne and Matthias Felleisen. Injecting Language Workbench Technology into Mainstream Languages. In Eelco Visser Commemorative Symposium (EVCS), 2023. URL: https://doi.org/10.4230/OASIcs.EVCS.2023.3.
  3. Michael Ballantyne, Mitch Gamburg, and Jason Hemann. Compiled, Extensible, Multi-Language DSLs (Functional Pearl). In International Conference on Functional Programming (ICFP), 2024. URL: https://doi.org/10.1145/3674627.
  4. H. Barringer, Y. Falcone, K. Havelund, G. Reger, and D. Rydeheard. Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors. In Formal Methods (FM), 2012. URL: https://doi.org/10.1007/978-3-642-32759-9_9.
  5. David Basin, Felix Klaedtke, and Eugen Zălinescu. The MonPoly Monitoring Tool. In Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES), 2017. URL: https://doi.org/10.29007/89hs.
  6. Eugene Burmako. Scala Macros: Let Our Powers Combine! In Workshop on Scala, 2013. URL: https://doi.org/10.1145/2489837.2489840.
  7. Feng Chen and Grigore Roşu. MOP: An Efficient and Generic Runtime Verification Framework. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2007. URL: https://doi.org/10.1145/1297027.1297069.
  8. William R. Cook. On Understanding Data Abstraction, Revisited. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2009. URL: https://doi.org/10.1145/1640089.1640133.
  9. Ryan Culpepper. Fortifying Macros. Journal of Functional Programming (JFP), 2012. URL: https://doi.org/10.1017/s0956796812000275.
  10. Ryan Culpepper and Matthias Felleisen. Fortifying Macros. In International Conference on Functional Programming (ICFP), 2010. URL: https://doi.org/10.1145/1863543.1863577.
  11. B. D'Angelo, S. Sankaranarayanan, C. Sanchez, W. Robinson, B. Finkbeiner, H.B. Sipma, S. Mehrotra, and Z. Manna. LOLA: Runtime Monitoring of Synchronous Systems. In Temporal Representation and Reasoning (TIME), 2005. URL: https://doi.org/10.1109/TIME.2005.26.
  12. Christos Dimoulas, Max S. New, Robert Bruce Findler, and Matthias Felleisen. Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl). In International Conference on Functional Programming (ICFP), 2016. URL: https://doi.org/10.1145/2951913.2951930.
  13. Sebastian Erdweg, Tillmann Rendel, Christian Kästner, and Klaus Ostermann. Sugarj: Library-Based Syntactic Language Extensibility. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2011. URL: https://doi.org/10.1145/2048066.2048099.
  14. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt. A Programmable Programming Language. Communications of the ACM (CACM), 2018. URL: https://doi.org/10.1145/3127323.
  15. 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 (JFP), 2002. URL: https://doi.org/10.1017/S0956796801004208.
  16. Robert Bruce Findler and Matthias Felleisen. Contracts for Higher-Order Functions. In International Conference on Functional Programming (ICFP), 2002. URL: https://doi.org/10.1145/581478.581484.
  17. Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay McCarthy, Sam Phillips, Sorawee Porncharoenwase, Jens Axel Søgaard, and Sam Tobin-Hochstadt. Rhombus: A New Spin on Macros without All the Parentheses. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2023. URL: https://doi.org/10.1145/3622818.
  18. Matthew Flatt, Eli Barzilay, and Robert Bruce Findler. Scribble: Closing the Book on Ad Hoc Documentation Tools. In International Conference on Functional Programming (ICFP), 2009. URL: https://doi.org/10.1145/1596550.1596569.
  19. Matthew Flatt and PLT. Reference: Racket. Technical Report PLT-TR-2010-1, PLT Design Inc., 2010. URL: https://racket-lang.org/tr1/.
  20. Jeremy Gibbons and Nicolas Wu. Folding Domain-Specific Languages: Deep and Shallow Embeddings (Functional Pearl). In International Conference on Functional Programming (ICFP), 2014. URL: https://doi.org/10.1145/2628136.2628138.
  21. Ben Greenman, Siddhartha Prasad, Antonio Di Stasio, Shufang Zhu, Giuseppe De Giacomo, Shriram Krishnamurthi, Marco Montali, Tim Nelson, and Milda Zizyte. Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic. In Formal Methods, 2024. URL: https://doi.org/10.1007/978-3-031-71162-6_30.
  22. Ben Greenman, Sam Saarinen, Tim Nelson, and Shriram Krishnamurthi. Little Tricky Logic: Misconceptions in the Understanding of LTL. The Art, Science, and Engineering of Programming, 2023. URL: https://doi.org/10.22152/programming-journal.org/2023/7/7.
  23. Rich Hickey. A History of Clojure. In History of Programming Languages (HOPL), 2020. URL: https://doi.org/10.1145/3386321.
  24. Dongyun Jin, Patrick O’Neil Meredith, Dennis Griffith, and Grigore Rosu. Garbage Collection for Monitoring Parametric Properties. In Programming Language Design and Implementation (PLDI), 2011. URL: https://doi.org/10.1145/1993498.1993547.
  25. Gregor Kiczales, Erik Hilsdale, Jim Hugunin, Mik Kersten, Jeffrey Palm, and William G. Griswold. An Overview of AspectJ. In European Conference on Object-Oriented Programming (ECOOP), 2001. URL: https://doi.org/10.1007/3-540-45337-7_18.
  26. S.C. Kleene. Representation of Events in Nerve Nets and Finite Automata. In Automata Studies. Princeton University Press, Princeton, N.J., 1956. URL: https://doi.org/10.1515/9781400882618-002.
  27. Lukas Lazarek, Ben Greenman, Matthias Felleisen, and Christos Dimoulas. How To Evaluate Blame For Gradual Types. In International Conference on Functional Programming (ICFP), 2021. URL: https://doi.org/10.1145/3473573.
  28. Lukas Lazarek, Ben Greenman, Matthias Felleisen, and Christos Dimoulas. How To Evaluate Blame For Gradual Types, Part 2. In International Conference on Functional Programming (ICFP), 2023. URL: https://doi.org/10.1145/3607836.
  29. Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, and Christos Dimoulas. Does Blame Shifting Work? In Principles of Programming Languages (POPL), 2020. URL: https://doi.org/10.1145/3371133.
  30. Owolabi Legunsen, Wajih Ul Hassan, Xinyue Xu, Grigore Roşu, and Darko Marinov. How Good are the Specs? A Study of the Bug-Finding Effectiveness of Existing Java API Specifications. In Automated Software Engineering (ASE), 2016. URL: https://doi.org/10.1145/2970276.2970356.
  31. Orna Lichtenstein, Amir Pnueli, and Lenore Zuck. The Glory Of The Past. In Logics of Programs, 1985. URL: https://doi.org/10.1007/3-540-15648-8_16.
  32. Patrick O'Neil Meredith, Dongyun Jin, Dennis Griffith, Feng Chen, and Grigore Roşu. An Overview of the MOP Runtime Verification Framework. International Journal on Software Tools for Technology Transfer, 2011. URL: https://doi.org/10.1007/s10009-011-0198-6.
  33. Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, 1988. Google Scholar
  34. Bertrand Meyer. Applying "Design by Contract". Computer, 1992. URL: https://doi.org/10.1109/2.161279.
  35. Scott Moore, Christos Dimoulas, Robert Bruce Findler, Matthew Flatt, and Stephen Chong. Extensible Access Control with Authorization Contracts. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2016. URL: https://doi.org/10.1145/2983990.2984021.
  36. Cameron Moy, Christos Dimoulas, and Matthias Felleisen. Effectful Software Contracts. In Principles of Programming Languages (POPL), 2024. URL: https://doi.org/10.1145/3632930.
  37. Cameron Moy and Matthias Felleisen. Trace Contracts. Journal of Functional Programming (JFP), 2023. URL: https://doi.org/10.1017/S0956796823000096.
  38. Phúc C. Nguy~ên, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn. Soft Contract Verification for Higher-Order Stateful Programs. In Principles of Programming Languages (POPL), 2018. URL: https://doi.org/10.1145/3158139.
  39. Oracle. Iterator(Java SE 23 & JDK 23). https://docs.oracle.com/en/java/javase/23/docs/api/java.base/java/util/Iterator.html, 2024.
  40. Oracle. Map (Java SE 23 & JDK 23). https://docs.oracle.com/en/java/javase/23/docs/api/java.base/java/util/Map.html, 2024.
  41. Terence Parr. Language Implementation Patterns: Create Your Own Domain-Specific and General Programming Languages. Pragmatic Bookshelf, 2009. Google Scholar
  42. The Rust Project. The Rust Reference: Procedural Macros. https://doc.rust-lang.org/reference/procedural-macros.html, 2024.
  43. M. O. Rabin and D. Scott. Finite Automata and their Decision Problems. IBM Journal of Research and Development, 1959. URL: https://doi.org/10.1147/rd.32.0114.
  44. Tiark Rompf and Martin Odersky. Lightweight Modular Staging: A Pragmatic Approach to Runtime Code Generation and Compiled DSLs. In Generative Programming and Component Engineering (GPCE), 2010. URL: https://doi.org/10.1145/1868294.1868314.
  45. Usa Sammapun and Oleg Sokolsky. Regular Expressions for Run-Time Verification. In Automated Technology for Verification and Analysis (ATVA), 2003. Google Scholar
  46. Michael Sperber, R. Kent Dybvig, Matthew Flatt, Anton Van Straaten, Robby Findler, and Jacob Matthews. Revised⁶ Report on the Algorithmic Language Scheme. Journal of Functional Programming, 2009. URL: https://doi.org/10.1017/s0956796809990074.
  47. Guy L. Steele. Common Lisp the Language. Digital Press, 1990. Google Scholar
  48. T. Stephen Strickland, Christos Dimoulas, Asumu Takikawa, and Matthias Felleisen. Contracts For First-Class Classes. Transactions on Programming Languages and Systems (TOPLAS), 2013. URL: https://doi.org/10.1145/2518189.
  49. T. Stephen Strickland, Brianna M. Ren, and Jeffrey S. Foster. Contracts For Domain-Specific Languages In Ruby. In Dynamic Languages Symposium (DLS), 2014. URL: https://doi.org/10.1145/2661088.2661092.
  50. T. Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt. Chaperones and Impersonators: Run-Time Support for Reasonable Interposition. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2012. URL: https://doi.org/10.1145/2384616.2384685.
  51. Tom Van Cutsem and Mark S. Miller. Proxies: Design Principles for Robust Object-oriented Intercession APIs. In Dynamic Languages Symposium (DLS), 2010. URL: https://doi.org/10.1145/1869631.1869638.
  52. Lucas Waye, Stephen Chong, and Christos Dimoulas. Whip: Higher-Order Contracts for Modern Services. In International Conference on Functional Programming (ICFP), 2017. URL: https://doi.org/10.1145/3110280.
  53. Dana N. Xu, Simon Peyton Jones, and Koen Claessen. Static Contract Checking for Haskell. In Principles of Programming Languages (POPL), 2009. URL: https://doi.org/10.1145/1480881.1480889.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact