Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

We describe an automated analysis of Haskell 98 programs to check statically that, despite the possible use of partial (or non-exhaustive) pattern matching, no pattern-match failure can occur. Our method is an iterative backward analysis using a novel form of pattern-constraint to represent sets of data values. The analysis is defined for a core first-order language to which Haskell 98 programs are reduced. Our analysis tool has been successfully applied to a range of programs, and our techniques seem to scale well. Throughout the paper, methods are represented much as we have implemented them in practice, again in Haskell.

REFERENCES

• 1: Stephen Adams. Efficient sets - a balancing act. JFP, 3 (4): 553--561, 1993.
• 2: Alex Aiken , Brian Murphy, Static type inference in a dynamically typed language, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.279-290, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99621]
• 3: John Horton Conway. Regular Algebra and Finite Machines. London Chapman and Hall, 1971.
• 4: Matthew Fluet , Riccardo Pucella, Phantom Types and Subtyping, Proceedings of the IFIP 17th World Computer Congress - TC1 Stream / 2nd IFIP International Conference on Theoretical Computer Science: Foundations of Information Technology in the Era of Networking and Mobile Computing, p.448-460, August 25-30, 2002
• 5: Dimitry Golubovsky, Neil Mitchell, and Matthew Naylor. Yhc.Core - from Haskell to Core. The Monad.Reader, 1 (7): 45--61, April 2007.
• 6: S. C. Johnson. Lint, a C program checker. Technical Report 65, Bell Laboratories, 1978.
• 7: C. Lee. Representation of switching circuits by binary decision diagrams. Bell System Technical Journal, 38: 985--999, 1959.
• 8: Tobias Lindahl and Konstantinos Sagonas. Detecting software defects in telecom applications through lightweight static analysis: A war story. In Proc. APLAS '04, LNCS 3302, pages 91--106. Springer, November 2004.
• 9: Luc Maranget. Warnings for pattern matching. JFP, 17 (3): 1--35, May 2007.
• 10: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 11: Neil Mitchell. Transformation and Analysis of Functional Programs. PhD thesis, University of York, 2008.
• 12: Neil Mitchell and Colin Runciman. A static checker for safe pattern matching in Haskell. In Trends in Functional Programming (2005 Symposium), volume 6, pages 15--30. Intellect, 2007.
• 13: Matthew Naylor , Colin Runciman, Finding Inputs that Reach a Target Expression, Proceedings of the Seventh IEEE International Working Conference on Source Code Analysis and Manipulation, p.133-142, September 30-October 01, 2007 [doi>10.1109/SCAM.2007.11]
• 14: Will Partain, The nofib Benchmark Suite of Haskell Programs, Proceedings of the 1992 Glasgow Workshop on Functional Programming, p.195-202, July 06-08, 1992
• 15: Simon Peyton Jones. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.
• 16: Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , Geoffrey Washburn, Simple unification-based type inference for GADTs, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA [doi>10.1145/1159803.1159811]
• 17: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 18: David Roundy, Darcs: distributed version management in haskell, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, p.1-4, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088348.1088349]
• 19: 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]
• 20: Don Stewart , Spencer Sjanssen, Xmonad, Proceedings of the ACM SIGPLAN workshop on Haskell workshop, September 30-30, 2007, Freiburg, Germany [doi>10.1145/1291201.1291218]
• 21: The GHC Team. The GHC compiler, version 6.8.2. http://www.haskell.org/ghc/, December 2007.
• 22: Andrew Tolmach. An External Representation for the GHC Core Language. http://www.haskell.org/ghc/docs/papers/core.ps.gz, September 2001.
• 23: Akihiko Tozawa, Towards static type checking for XSLT, Proceedings of the 2001 ACM Symposium on Document engineering, November 09-10, 2001, Atlanta, Georgia, USA [doi>10.1145/502187.502191]
• 24: David Turner. Total Functional Programming. Journal of Universal Computer Science, 10 (7): 751--768, July 2004.
• 25: Joe Armstrong , Robert Virding , Claes Wikström , Mike Williams, Concurrent programming in ERLANG (2nd ed.), Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1996
• 26: 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]
• 27: 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]
• 28: Dana N. Xu, Simon Peyton Jones, and Koen Claessen. Static contract checking for Haskell. In Proc. IFL 2007, pages 382--399, 2007.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Languages, Verification

Keywords:
automatic verification, functional programming, haskell, pattern-match errors, preconditions