Static contract checking for Haskell

ABSTRACT

Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and for systems that are guarded by runtime checks. Static verification techniques have been applied to imperative and object-oriented languages, like Java and C#, but few have been applied to a higher-order lazy functional language, like Haskell. In this paper, we describe a sound and automatic static verification framework for Haskell, that is based on contracts and symbolic execution. Our approach is modular and gives precise blame assignments at compile-time in the presence of higher-order functions and laziness.

REFERENCES

• 1: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 2: Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. CASSIS, LNCS 3362, 2004.
• 3: Matthias Blume , David McAllester, Sound and complete models of contracts, Journal of Functional Programming, v.16 n.4-5, p.375-414, July 2006 [doi>10.1017/S0956796806005971]
• 4: L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. Leavens, K. Leino, and E. Poll. An overview of JML tools and applications, 2003.
• 5: Koen Claessen and John Hughes. Specification-based testing with QuickCheck. In Fun of Programming, Cornerstones of Computing, pages 17--40. Palgrave, March 2003.
• 6: Sa Cui, Kevin Donnelly, and Hongwei Xi. ATS: A language that combines programming with theorem proving. In Bernhard Gramlich, editor, FroCos, volume 3717 of Lecture Notes in Computer Science, pages 310--320. Springer, 2005.
• 7: Rowan Davies, Refinement-Type Checker for Standard ML, Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology, p.565-566, December 13-17, 1997
• 8: Peter Dybjer , Qiao Haiyan , Makoto Takeyama, Verifying Haskell Programs by Combining Testing and Proving, Proceedings of the Third International Conference on Quality Software, p.272, November 06-07, 2003
• 9: R. B. Findler, M. Blume, and M. Felleisen. An investigation of contracts as projections. Technical report, University of Chicago Computer Science Department, 2006. Technical Report TR-2004-02.
• 10: Robert Bruce Findler and Matthias Blume. Contracts as pairs of projections. In Functional and Logic Programming, pages 226--241. Springer Berlin / Heidelberg, 2006.
• 11: Robert Bruce Findler , Matthias Felleisen, Contracts for higher-order functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.48-59, October 04-06, 2002, Pittsburgh, PA, USA
• 12: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA
• 13: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 14: Cormac Flanagan , James B. Saxe, Avoiding exponential explosion: generating compact verification conditions, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.193-205, January 2001, London, United Kingdom
• 15: Tim Freeman , Frank Pfenning, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.268-277, June 24-28, 1991, Toronto, Ontario, Canada
• 16: Jessica Gronski and Cormac Flanagan. Unifying hybrid types and contracts. In Eighth Symposium on Trends in Functional Programming, April 2007.
• 17: Thomas Hallgren, Haskell tools from the programatica project, Proceedings of the 2003 ACM SIGPLAN workshop on Haskell, p.103-106, August 28-28, 2003, Uppsala, Sweden [doi>10.1145/871895.871907]
• 18: Ralf Hinze, Johan Jeuring, and Andres Löh. Typed contracts for functional programming. In Functional and Logic Programming: 8th International Symposium, pages 208--225, 2006.
• 19: Kohei Honda , Nobuko Yoshida, A compositional logic for polymorphic higher-order functions, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.191-202, August 24-26, 2004, Verona, Italy [doi>10.1145/1013963.1013985]
• 20: Kenneth Knowles and Cormac Flanagan. Type reconstruction for general refinement types. In ESOP '07: Programming Languages and Systems, 16th European Symposium on Programming. Springer-Verlag, April 2007.
• 21: Kenneth Knowles, Aaron Tomb, Jessica Gronski, Stephen N. Freund, and Cormac Flanagan. SAGE: Unified hybrid checking for first--class types, general refinement types, and dynamic (extended report). Technical report, UC Santa Cruz, 2006. http://sage.soe.ucsc.edu/sage-tr.pdf.
• 22: K. Rustan M. Leino , Greg Nelson, An Extended Static Checker for Modular-3, Proceedings of the 7th International Conference on Compiler Construction, p.302-305, March 28-April 04, 1998
• 23: Philippe Meunier, Robert Bruce Findler, and Matthias Felleisen. Modular set-based analysis from contracts. In Morrisett and Peyton Jones {27}, pages 218--231.
• 24: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 25: Neil Mitchell. Transformation and Analysis of Functional Programs. PhD thesis, University of York, 2008.
• 26: Neil Mitchell , Colin Runciman, Not all patterns, but enough: an automatic verifier for partial but sufficient pattern matching, Proceedings of the first ACM SIGPLAN symposium on Haskell, September 25-25, 2008, Victoria, BC, Canada
• 27: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 2006
• 28: Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, and Lars Birkedal. Abstract predicates and mutable ADTs in Hoare Type Theory. In Rocco De Nicola, editor, ESOP, volume 4421 of Lecture Notes in Computer Science, pages 189--204. Springer, 2007.
• 29: Aleksandar Nanevski , Greg Morrisett , Lars Birkedal, Polymorphism and separation in hoare type theory, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 30: D. L. Parnas, A technique for software module specification with examples, Communications of the ACM, v.15 n.5, p.330-336, May 1972 [doi>10.1145/355602.361309]
• 31: Yann Régis-Gianas , François Pottier, A Hoare Logic for Call-by-Value Functional Programs, Proceedings of the 9th international conference on Mathematics of Program Construction, p.305-335, July 15-18, 2008, Marseille, France [doi>10.1007/978-3-540-70594-9_17]
• 32: Tim Sheard, Languages of the future, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028711]
• 33: The GHC Team. The Glasgow Haskell Compiler user's guide. www.haskell.org/ghc/documentation.html, 1998.
• 34: J Visser, J. N. Oliveira, Barbosa L. S., J. F. Ferreira, and A. Mendes. CAMILA revival: VDM meets Haskell. In Nico Plat and Peter Gorm Larsen, editors, Overture Workshop (co-located with FM'05), 2005.
• 35: Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In Workshop on Scheme and Functional Programming, Sept 2007.
• 36: Edwin Westbrook , Aaron Stump , Ian Wehrman, A language-based approach to functionally correct imperative programming, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 37: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]
• 38: Dana N. Xu, Extended static checking for haskell, Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, September 17-17, 2006, Portland, Oregon, USA [doi>10.1145/1159842.1159849]
• 39: Na Xu. Static Contract Checking for Haskell. PhD thesis, University of Cambridge, 2008. http://www.cl.cam.ac.uk/techreports/.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Verification

Keywords:
contract satisfaction, static contract checking