SmartCheck: Automatic and Efficient Counterexample Reduction and Generalization

QuickCheck is a powerful library for automatic test-case genera-tion. Because QuickCheck performs random testing, some of the counterexamples discovered are very large. QuickCheck provides an interface for the user to write shrink functions to attempt to re-duce the size of counterexamples. Hand-written implementations of shrink can be complex, inefficient, and consist of significant boilerplate code. Furthermore, shrinking is only one aspect in de-bugging: counterexample generalization is the process of extrapo-lating from individual counterexamples to a class of counterexam-ples, often requiring a flash of insight from the programmer. To im-prove counterexample reduction and generalization, we introduce SmartCheck. SmartCheck is a debugging tool that reduces alge-braic data using generic search heuristics to efficiently find smaller counterexamples. In addition to shrinking, SmartCheck also au-tomatically generalizes counterexamples to formulas representing classes of counterexamples. SmartCheck has been implemented for Haskell and is freely available