Skip to main content
SpringerLink
Log in

Contracts as Pairs of Projections

  • Conference paper
Functional and Logic Programming (FLOPS 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3945))

Included in the following conference series:

Abstract

Assertion-based contracts provide a powerful mechanism for stating invariants at module boundaries and for enforcing them uniformly. In 2002, Findler and Felleisen showed how to add contracts to higher-order functional languages, allowing programmers to assert invariants about functions as values. Following up in 2004, Blume and McAllester provided a quotient model for contracts. Roughly speaking, their model equates a contract with the set of values that cannot violate the contract. Their studies raised interesting questions about the nature of contracts and, in particular, the nature of the any contract.

In this paper, we develop a model for software contracts that follows Dana Scott’s program by interpreting contracts as projections. The model has already improved our implementation of contracts. We also demonstrate how it increases our understanding of contract-oriented programming and design. In particular, our work provides a definitive answer to the questions raised by Blume and McAllester’s work. The key insight from our model that resolves those questions is that a contract that puts no obligation on either party is not the same as the most permissive contract for just one of the parties.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bartetzko, D.: Parallelität und Vererbung beim Programmieren mit Vertrag. Diplomarbeit, Universität Oldenburg (April 1999)

    Google Scholar 

  2. Blume, M., McAllester, D.: Sound and complete models of contracts. Journal of Functional Programming (to appear)

    Google Scholar 

  3. Carrillo-Castellon, M., Garcia-Molina, J., Pimentel, E., Repiso, I.: Design by contract in Smalltalk. Journal of Object-Oriented Programming 7(9), 23–28 (1996)

    Google Scholar 

  4. Cheon, Y.: A runtime assertion checker for the Java Modelling Language. Technical Report 03-09, Iowa State University Computer Science Department (April 2003)

    Google Scholar 

  5. Conway, D., Goebel, C.G.: Class:Contract – design-by-contract OO in Perl, http://search.cpan.org/~ggoebel/Class-Contract-1.14/

  6. Danvy, O., Nielsen, L.R.: Defunctionalization at work. In: International Conference on Principles and Practice of Declarative Programming (2001)

    Google Scholar 

  7. Duncan, A., Hölzle, U.: Adding contracts to Java with handshake. Technical Report TRCS98-32, The University of California at Santa Barbara (December 1998)

    Google Scholar 

  8. Dybvig, R.K., Hieb, R., Bruggeman, C.: Syntactic abstraction in Scheme. Lisp and Symbolic Computation 5(4), 295–326 (1993)

    Article  Google Scholar 

  9. Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 235–271 (1992)

    Google Scholar 

  10. Findler, B., Blume, C., Felleisen, F., Huang, M., McCarthy, S., Press, R., Reppy, R., Spiro, T., Wick: The eighth annual ICFP programming contest, http://icfpc.plt-scheme.org/

  11. Findler, R.B., Blume, M.: Contracts as pairs of projections. Technical Report TR- 2006-01, University of Chicago Computer Science Department (2006), http://www.cs.uchicago.edu/research/publications/techreports/TR-2006-01

  12. Findler, R.B., Blume, M., Felleisen, M.: An investigation of contracts as projections. Technical Report TR-2004-02, University of Chicago Computer Science Department (2004)

    Google Scholar 

  13. Findler, R.B., Felleisen, M.: Contract soundness for object-oriented languages. In: Object-Oriented Programming, Systems, Languages, and Applications (2001)

    Google Scholar 

  14. Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: Proceedings of ACM SIGPLAN International Conference on Functional Programming (2002)

    Google Scholar 

  15. Findler, R.B., Flatt, M., Felleisen, M.: Semantic casts: Contracts and structural subtyping in a nominal world. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 365–389. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. Findler, R.B., Latendresse, M., Felleisen, M.: Behavioral contracts and behavioral subtyping. In: Proceedings of ACM Conference Foundations of Software Engineering (2001)

    Google Scholar 

  17. Flatt, M.P.: Language manual. Technical Report TR97-280, Rice University (1997), http://www.mzscheme.org/

  18. Gray, K.E., Findler, R.B., Flatt, M.: Fine-grained interoperability through contracts and mirrors. In: Object-Oriented Programming, Systems, Languages, and Applications (2005)

    Google Scholar 

  19. Jones, S.P., Washburn, G., Weirich, S.: Wobbly types: Practical type inference for generalized algebraic dataypes, http://www.cis.upenn.edu/~sweirich/publications.html

  20. Karaorman, M., Hölzle, U., Bruno, J.: jContractor: A reflective java library to support design by contract. In: Cointe, P. (ed.) Reflection 1999. LNCS, vol. 1616, p. 175. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  21. Kelsey, R., Clinger, W., Rees, J. (eds.): Revised5 report of the algorithmic language Scheme; Higher-Order and Symbolic Computation 11(1), 7–105 (1998); Also appears in ACM SIGPLAN Notices 33(9) (September 1998)

    Google Scholar 

  22. Kiniry, J.R., Cheong, E.: JPP: A Java pre-processor. Technical Report CS-TR-98-15, Department of Computer Science, California Institute of Technology (1998)

    Google Scholar 

  23. Kohlbecker, E.E., Friedman, D.P., Felleisen, M., Duba, B.F.: Hygienic macro expansion. In: ACM Symposium on Lisp and Functional Programming, pp. 151–161 (1986)

    Google Scholar 

  24. Kramer, R.: iContract: The Java design by contract tool. In: Technology of Object-Oriented Languages and Systems (1998)

    Google Scholar 

  25. Launchbury, J.: Projections factorizations in partial evaluation. Cambridge University Press, Cambridge (1991)

    Book  MATH  Google Scholar 

  26. Man Machine Systems. Design by contract for Java using JMSAssert (2000), http://www.mmsindia.com/

  27. Matthews, J., Findler, R.B.: An operational semantics for R5RS Scheme. In: Workshop on Scheme and Functional Programming (2005)

    Google Scholar 

  28. McCarthy, J.: A basis for a mathematical theory of computation. Computer Programming and Formal Systems (1961), http://www-formal.stanford.edu/jmc/basis/basis.html

  29. McFarlane, K.: Design by contract framework, http://www.codeproject.com/csharp/designbycontract.asp

  30. Meyer, B.E.: The Language. Prentice-Hall, Englewood Cliffs (1992)

    MATH  Google Scholar 

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

    Article  Google Scholar 

  32. Plösch, R.: Design by contract for Python. In: IEEE Proceedings of the Joint Asia Pacific Software Engineering Conference (1997), http://citeseer.nj.nec.com/257710.html

  33. Plösch, R., Pichler, J.: Contracts: From analysis to C++ implementation. In: Technology of Object-Oriented Languages and Systems, pp. 248–257 (1999)

    Google Scholar 

  34. Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1, 125–159 (1975), http://homepages.inf.ed.ac.uk/gdp/publications/cbncbvlambda.pdf

    Article  MathSciNet  MATH  Google Scholar 

  35. PLT. PLT MzLib: Libraries manual. Technical Report PLT-TR05-4-v300, PLT Scheme Inc. (2005), http://www.plt-scheme.org/techreports/

  36. Reynolds, J.C.: Definitional interpreters for higher-order programming languages. Higher- Order and Symbolic Computation 11(4), 363–397 (1998); Reprinted from the proceedings of the 25th ACM National Conference (1972), with a foreword

    Google Scholar 

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

    Article  Google Scholar 

  38. Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation 6(3/4), 289–360 (1993)

    Article  Google Scholar 

  39. Scott, D.S.: Data types as lattices. Society of Industrial and Applied Mathematics (SIAM) Journal of Computing 5(3), 522–586 (1976)

    MathSciNet  MATH  Google Scholar 

  40. The GHC Team. Glasgow Haskell compiler, http://www.haskell.org/ghc/

  41. Wadler, P., Hughes, R.J.M.: Projections for Strictness Analysis. In: Kahn, G. (ed.) FPCA 1987. LNCS, vol. 274, pp. 385–407. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  42. Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: Proceedings of the ACM Conference Principles of Programming Languages (2003)

    Google Scholar 

  43. Yang, Z.: Encoding types in ml-like languages. In: Proceedings of ACM SIGPLAN International Conference on Functional Programming (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Chicago, USA

    Robert Bruce Findler

  2. Toyota Technological Institute at Chicago, USA

    Matthias Blume

Authors
  1. Robert Bruce Findler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matthias Blume
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NTT Communication Science Laboratories, Japan

    Masami Hagiya

  2. University of Edinburgh, UK

    Philip Wadler

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Findler, R.B., Blume, M. (2006). Contracts as Pairs of Projections. In: Hagiya, M., Wadler, P. (eds) Functional and Logic Programming. FLOPS 2006. Lecture Notes in Computer Science, vol 3945. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11737414_16

Download citation

  • DOI: https://doi.org/10.1007/11737414_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-33438-5

  • Online ISBN: 978-3-540-33439-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation