Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry SpecCheck

view this post on Zulip Email Gateway (Jul 08 2021 at 19:30):

From: Andreas Lochbihler <>
Dear all,

I'm happy to announce the new AFP entry SpecCheck by Kevin Kappelmann, Lukas Bulwahn, and
Sebastian Willenbrink.

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.

Great to see that we can now sanity-check our ML functions similarly to what quickcheck
does for our theorems!


Last updated: Jan 25 2022 at 02:35 UTC