ABSTRACT
Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and to systems that are guarded by runtime checks. Extended static checking can reduce these costs by helping to detect bugs at compile-time, where possible. Extended static checking has been applied to objectoriented languages, like Java and C#, but it has not been applied to a lazy functional language, like Haskell. In this paper, we describe an extended static checking tool for Haskell, named ESC/Haskell, that is based on symbolic computation and assisted by a few novel strategies. One novelty is our use of Haskell as the specification language itself for pre/post conditions. Any Haskell function (including recursive and higher order functions) can be used in our specification which allows sophisticated properties to be expressed. To perform automatic verification, we rely on a novel technique based on symbolic computation that is augmented by counter-example guided unrolling. This technique can automate our verification process and be efficiently implemented.
- Lennart Augustsson. Cayenne - language with dependent types. In ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming, pages 239--250, New York, NY, USA, 1998. ACM Press. Google ScholarDigital Library
- Thomas Ball and Sriram K. Rajamani. The SLAMproject: debugging system software via static analysis. In POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 1--3, New York, NY, USA, 2002. ACM Press. Google ScholarDigital Library
- Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. CASSIS, LNCS 3362, 2004. Google ScholarDigital Library
- Koen Claessen and John Hughes. Specification-based testing with QuickCheck, volume Fun of Programming of Cornerstones of Computing, chapter 2, pages 17--40. Palgrave, March 2003.Google Scholar
- David Detlefs, Greg Nelson, and James B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3):365--473, 2005. Google ScholarDigital Library
- Peter Dybjer, Qiao Haiyan, and Makoto Takeyama. Verifying Haskell programs by combining testing and proving. In Proceedings of Third International Conference on Quality Software, pages 272--279. IEEE Press, 2003. Google ScholarDigital Library
- Robert Bruce Findler and Matthias Felleisen. Contracts for higherorder functions. In ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pages 48--59, New York, NY, USA, 2002. ACM Press. Google ScholarDigital Library
- Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pages 234--245, New York, NY, USA, 2002. ACM Press. Google ScholarDigital Library
- Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 193--205, New York, NY, USA, 2001. ACM Press. Google ScholarDigital Library
- Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Counterexample-guided control. Automata, Languages and Programming: 30th International Colloquium, (ICALP03), 2719:886--902, 2003. Google ScholarDigital Library
- Ralf Hinze, Johan Jeuring, and Andres Löh. Typed contracts for functional programming. In FLOPS '06: Functional and Logic Programming: 8th International Symposium, pages 208--225, 2006. Google ScholarDigital Library
- Kohei Honda and Nobuko Yoshida. A compositional logic for polymorphic higher-order functions. In PPDP '04: Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, pages 191--202, New York, NY, USA, 2004. ACM Press. Google ScholarDigital Library
- James Hook, Mark Jones, Richard Kieburtz, John Matthews, Peter White, Thomas Hallgren, and Iavor Diatchki. Programatica. http://www.cse.ogi.edu/PacSoft/projects/programatica/bodynew.htm, 2005.Google Scholar
- K. Rustan M. Leino and Greg Nelson. An extended static checker for Modular-3. In CC '98: Proceedings of the 7th International Conference on Compiler Construction, pages 302--305, London, UK, 1998. Springer-Verlag. Google ScholarDigital Library
- Neil Mitchell and Colin Runciman. Unfailing Haskell: A static checker for pattern matching. In TFP '05: The 6th Symposium on Trends in Functional Programming, pages 313--328, 2005.Google Scholar
- Andrew Moran and David Sands. Improvement in a lazy context: an operational theory for call-by-need. In POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 43--56, New York, NY, USA, 1999. ACM Press. Google ScholarDigital Library
- Simon L. Peyton Jones. Compiling Haskell by program transformation: A report from the trenches. In Proc European Symposium on Programming (ESOP), pages 18--44, 1996. Google ScholarDigital Library
- Tim Sheard. Languages of the future. In OOPSLA '04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, pages 116--119, New York, NY, USA, 2004. ACM Press. Google ScholarDigital Library
- The GHC Team. The Glasgow Haskell Compiler User's Guide. www.haskell.org/ghc/documentation.html, 1998.Google Scholar
- Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In POPL '99: Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages, pages 214--227, New York, NY, USA, 1999. ACM Press. Google ScholarDigital Library
- Dana N. Xu. Extended static checking for Haskell - technical report. http://www.cl.cam.ac.uk/users/nx200/research/escH-tr.ps, 2006.Google Scholar
Index Terms
- Extended static checking for haskell
Recommendations
Static contract checking for Haskell
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesProgram 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 ...
Extended static checking in JML4: benefits of multiple-prover support
SAC '09: Proceedings of the 2009 ACM symposium on Applied ComputingThe implementations of many seemingly simple algorithms are beyond the ability of traditional Extended Static Checking (ESC) tools to verify. Not being able to verify toy examples is often enough to turn users off of the idea of using formal methods. ...
Hybrid contract checking via symbolic simplification
PEPM '12: Proceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and program manipulationProgram errors are hard to detect or prove absent. Allowing programmers to write formal and precise specifications, especially in the form of contracts, is a popular approach to program verification and error discovery. We formalize and implement a ...
Comments