SpecCheck - Specification-Based Testing for Isabelle/ML (Q7361511)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry SpecCheck
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | SpecCheck - Specification-Based Testing for Isabelle/ML |
AFP entry SpecCheck |
Statements
1 July 2021
0 references
Kevin Kappelmann
0 references
Lukas Bulwahn
0 references
Sebastian Willenbrink
0 references
SpecCheck - Specification-Based Testing for Isabelle/ML (English)
0 references
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.
0 references
