Christos Dimoulas
Robert Bruce Findler
Cormac Flanagan
Matthias Felleisen
ABSTRACT
Behavioral software contracts supplement interface information with logical assertions. A rigorous enforcement of contracts provides useful feedback to developers if it signals contract violations as soon as they occur and if it assigns blame to violators with preciseexplanations. Correct blame assignment gets programmers started with the debugging process and can significantly decrease the time needed to discover and fix bugs.
Sadly the literature on contracts lacks a framework for making statements about the correctness of blame assignment and for validating such statements. This paper fills the gap and uses the framework to demonstrate how one of the proposed semantics for higher-order contracts satisfies this criteria and another semantics occasionally assigns blame to the wrong module.
Concretely, the paper applies the framework to the lax enforcement of dependent higher-order contracts and the picky one. A higher-order dependent contract specifies constraints for the domain and range of higher-order functions and also relates arguments and results in auxiliary assertions. The picky semantics ensures that the use of arguments in the auxiliary assertion satisfies the domain contracts and the lax one does not. While the picky semantics discovers more contract violations than the lax one, it occasionally blames the wrong module. Hence the paper also introduces a third semantics, dubbed indy, which fixes the problems of the picky semantics without giving up its advantages.
Supplemental Material
- H. P. Barendregt. phThe Lambda Calculus -- Its Syntax and Semantics, volume 103 of phStudies in Logic and the Foundations of Mathematics. North-Holland, 1984.Google Scholar
- M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: an overview. In Construction and Analysis of Safe, Secure and Interoperable Smart Devices, pages 49--69, 2004. Google ScholarDigital Library
- A. Beugnard, J.-M. Jézéquel, N. Plouzeau, and D. Watkins. Making components contract aware. IEEE Computer, 32 (7): 38--45, July 1999. Google ScholarDigital Library
- M. Blume and D. McAllester. Sound and complete models of contracts. Journal of Functional Programming, 16 (4--5): 375--414, 2006. Google ScholarDigital Library
- R. Bose and J. Frew. Lineage retrieval for scientific data processing: a survey. ACM Computing Survey, 37 (1): 1--28, 2005. Google ScholarDigital Library
- J. Cheney, S. Chong, N. Foster, M. Seltzer, and S. Vansummeren. Provenance: a future history. In Proceeding of the 24th ACM SIGPLAN Conference Companion on Object Oriented Programming Systems Languages and Applications: Onward! Session (OOPSLA Onward!), pages 957--964, 2009. Google ScholarDigital Library
- O. Chitil, D. McNeill, and C. Runciman. Lazy assertions. In Revised Papers of the 15th International Workshop on Implementation of Functional Languages (IFL), pages 1--19, 2003. Google ScholarDigital Library
- M. Degen, P. Thiemann, and S. Wehr. Eager and delayed contract monitoring for call-by-value and call-by-name evaluation. Journal of Logic and Algebraic Programming, page to appear, 2010.Google Scholar
- D. E. Denning. A lattice model of secure information flow. Communications of the ACM, 19 (5): 236--243, 1976. Google ScholarDigital Library
- D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Technical Report 158, Compaq SRC Research Report, 1998.Google Scholar
- C. Dimoulas and M. Felleisen. On contract satisfaction in a higher-order world. ACM Transactions on Programming Languages and Systems. accepted (with revisions) for publication. Google ScholarDigital Library
- M. Felleisen, R. B. Findler, and M. Flatt. Semantics Engineering with PLT Redex. MIT Press, 2009. Google ScholarDigital Library
- R. B. Findler and M. Blume. Contracts as pairs of projections. In Proceedings of the 8th International Symposium on Functional and Logic Programming (FLOPS), pages 226--241, 2006. Google ScholarDigital Library
- R. B. Findler and M. Felleisen. Contracts for higher-order functions. In Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 48--59, 2002. Google ScholarDigital Library
- R. B. Findler, J. Clements, C. Flanagan, M. Flatt, S. Krishnamurthi, P. Steckler, and M. Felleisen. DrScheme: A programming environment for Scheme. J. Funct. Program., 12 (2): 159--182, Mar. 2002. Google ScholarDigital Library
- R. B. Findler, M. Felleisen, and M. Blume. An investigation of contracts as projections. Technical Report TR-2004-02, University of Chicago, Computer Science Department, 2004.Google Scholar
- C. Flanagan. Hybrid type checking. In Proceedings of the 33th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 245--256, 2006. Google ScholarDigital Library
- M. Flatt and PLT. Reference: Racket. Technical Report PLT-TR-2010-1, PLT Inc., 2010. http://racket-lang.org/tr1/.Google Scholar
- M. Greenberg, B. C. Pierce, and S. Weirich. Contracts made manifest. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Programming Languages (POPL), pages 353--364, 2010. Google ScholarDigital Library
- J. Gronski and C. Flanagan. Unifying hybrid types and contracts. In Proceedings of the 8th Symposium on Trends in Functional Programming (TFP), pages 54--69, 2007.Google Scholar
- R. Hinze, J. Jeuring, and A. Löh. Typed contracts for functional programming. In In Proceedings of the 8th International Symposium on Functional and Logic Programming (FLOPS), pages 208--235, 2006. Google ScholarDigital Library
- K. Knowles, A. Tomb, J. Gronski, S. N. Freund, and C. Flanagan. Sage: Unified hybrid checking for first-class types, general refinement types, and dynamic, 2006. URL http://sage.soe.ucsc.edu/.Google Scholar
- G. T. Leavens, A. L. Baker, and C. Ruby. JML: A notation for detailed design. In H. Kilov, B. Rumpe, and I. Simmonids, editors, Behavioral Specifications of Businesses and Systems, pages 175--188. Kluwer Academic Publishers, 1999.Google ScholarCross Ref
- B. Meyer. Design by contract. In Advances in Object-Oriented Software Engineering, pages 1--50. Prentice Hall, 1991.Google Scholar
- B. Meyer. Eiffel: The Language. Prentice Hall, 1992. Google ScholarDigital Library
- B. Meyer. Object-oriented Software Construction. Prentice Hall, 1988. Google ScholarDigital Library
- G. D. Plotkin. Call-by-name, call-by-value, and the λ-calculus. Theoretical Computer Science, 1 (2): 125--159, 1975.Google ScholarCross Ref
- G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5 (3): 223--255, 1977.Google ScholarCross Ref
- A. Rudich, A. Darvas, and P. Müller. Checking well-formedness of pure-method specifications. In Proceedings of the 15th International Symposium on Formal Methods (FM), pages 68--83, 2008. Google ScholarDigital Library
- D. S. Scott. Data types as lattices. SIAM Journal of Computing, 5 (3): 522--587, 1976.Google ScholarCross Ref
- Y. L. Simmhan, B. Plale, and D. Gannon. A survey of data provenance in e-science. ACM SIGMOD Record, 34 (3): 31--36, 2005. Google ScholarDigital Library
- T. S. Strickland and M. Felleisen. Contracts for first-class modules. In Proceedings of the 5th Symposium on Dynamic Languages (DLS), pages 27--38. ACM, 2009. Google ScholarDigital Library
- S. Tobin-Hochstadt and M. Felleisen. Logical types for untyped languages. In Proceedings of the 15th ACM SIGPLAN Internation Conference on Functional Programming (ICFP), pages 117--128, 2010. Google ScholarDigital Library
- S. Tobin-Hochstadt and M. Felleisen. The design and implementation of Typed Scheme. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on the Pronciples of Programming Languages (POPL), pages 395--407, 2008. Google ScholarDigital Library
- D. Xu, S. Peyton Jones, and K. Claessen. Static contract checking for Haskell. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Programming Languages (POPL), pages 41--52, 2009. Google ScholarDigital Library
- S. Zdancewic, D. Grossman, and G. Morrisett. Principals in programming languages: A syntactic proof technique. In Proceedings of the 4th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 197--207, 1999. Google ScholarDigital Library
Index Terms
- Correct blame for contracts: no more scapegoating
Recommendations
Correct blame for contracts: no more scapegoating
POPL '11Behavioral software contracts supplement interface information with logical assertions. A rigorous enforcement of contracts provides useful feedback to developers if it signals contract violations as soon as they occur and if it assigns blame to ...
Complete monitors for behavioral contracts
ESOP'12: Proceedings of the 21st European conference on Programming Languages and SystemsA behavioral contract in a higher-order language may invoke methods of unknown objects. Although this expressive power allows programmers to formulate sophisticated contracts, it also poses a problem for language designers. Indeed, two distinct ...
Temporal higher-order contracts
ICFP '11Behavioral contracts are embraced by software engineers because they document module interfaces, detect interface violations, and help identify faulty modules (packages, classes, functions, etc). This paper extends prior higher-order contract systems to ...
Comments