Abstract
SpecCheck is a QuickCheck-like
testing framework for Isabelle/ML. You can use it to write
specifications for ML functions. SpecCheck then checks whether your
specification holds by testing your function against a given number of
generated inputs. It helps you to identify bugs by printing
counterexamples on failure and provides you timing information.
SpecCheck is customisable and allows you to specify your own input
generators, test output formats, as well as pretty printers and
shrinking functions for counterexamples among other things.