Testing monadic code with QuickCheck

ABSTRACT

QuickCheck is a previously published random testing tool for Haskell programs. In this paper we show how to use it for testing monadic code, and in particular imperative code written using the ST monad. QuickCheck tests a program against a specification: we show that QuickCheck's specification language is sufficiently powerful to represent common forms of specifications: algebraic, model-based (both functional and relational), and pre-/post-conditional. Moreover, all these forms of specification can be used directly for testing. We define a new language of monadic properties, and make a link between program testing and the notion of observational equivalence.

REFERENCES

• 1: S. Antoy and R. Hamlet. Automatically checking an implementation against its formal specification. In Irvine Software Symposium, pages 29-48, March 1992.
• 2: Gilles Bernot , Marie Claude Gaudel , Bruno Marre, Software testing based on formal specifications: a theory and a tool, Software Engineering Journal, v.6 n.6, p.387-405, Nov. 1991
• 3: F. Warren Burton. An efficient functional implementation of FIFO queues. Information Processing Letters, 14(5):205-206, July 1982.
• 4: Koen Claessen , John Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.268-279, September 2000
• 5: Michael R. Donat, Automating Formal Specification-Based Testing, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.833-847, April 14-18, 1997
• 6: J. Duran and S. Ntafos. An evaluation of random testing. Transactions on Software Engineering, 10(4):438-444, July 1984.
• 7: Stephen H. Edwards. A framework for practical, automated black-box testing of component-base software. Software Testing, Verification and Reliability, 11(2), June 2001.
• 8: John Gannon , Paul McMullin , Richard Hamlet, Data Abstraction, Implementation, Specification, and Testing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.3, p.211-223, July 1981 [doi>10.1145/357139.357140]
• 9: D. Hamlet. Random testing. In J. Marciniak, editor, Encyclopedia of Software Engineering, pages 970-978. Wiley, 1994.
• 10: Dick Hamlet , Ross Taylor, Partition Testing Does Not Inspire Confidence (Program Testing), IEEE Transactions on Software Engineering, v.16 n.12, p.1402-1411, December 1990 [doi>10.1109/32.62448]
• 11: Ian Hayes, Specification case studies, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1987
• 12: Dean Herington. HUnit 1.0 User's Guide, 2002. http://hunit.sourceforge.net/HUnit-1.0/Guide.html.
• 13: P. Hudak, Modular Domain Specific Languages and Tools, Proceedings of the 5th International Conference on Software Reuse, p.134, June 02-05, 1998
• 14: Simon Peyton Jones. Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In Tony Hoare, Manfred Broy, and Ralf Steinbruggen, editors, Engineering theories of software construction, pages 47-96. IOS Press, 2001. Presented at the 2000 Marktoberdorf Summer School.
• 15: John Launchbury , Simon L. Peyton Jones, State in Haskell, Lisp and Symbolic Computation, v.8 n.4, p.293-341, Dec. 1995 [doi>10.1007/BF01018827]
• 16: Sheng Liang , Paul Hudak , Mark Jones, Monad transformers and modular interpreters, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.333-343, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199528]
• 17: Tom Moertel. Seven Lessons from the ICFP Programming Contest. http://www.kuro5hin.org/story/2001/7/31/0102/11014, 2001.
• 18: Graeme E. Moss , Colin Runciman, Automated Benchmarking of Functional Data Structures, Proceedings of the First International Workshop on Practical Aspects of Declarative Languages, p.1-15, January 18-19, 1999
• 19: Nigel Tracey , John Penix , Willem C. Visser, The First International Workshop on Automated Program Analysis, Testing and Verification (workshop session), Proceedings of the 22nd international conference on Software engineering, p.796, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337819]
• 20: Martin Odersky , Konstantin Läufer, Putting type annotations to work, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-67, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237729]
• 21: Chris Okasaki. An Overview of Edison. In Haskell Workshop, pages 34-54, September 2000.
• 22: Simon L. Peyton Jones , Philip Wadler, Imperative functional programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-84, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158524]
• 23: Andrew M. Pitts. Evaluation logic. In G. Birtwistle, editor, Proceedings of the IVth Higher Order Workshop, pages 162-189. Springer-Verlag, 1990.
• 24: Phil Stocks , David Carrington, A Framework for Specification-Based Testing, IEEE Transactions on Software Engineering, v.22 n.11, p.777-793, November 1996 [doi>10.1109/32.553698]
• 25: Malcolm Wallace, Olaf Chitil, Thorsten Brehm, and Colin Runciman. Multiple-View Tracing for Haskell: a New Hat. In Haskell Workshop. ACM, September 2001.