### 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.

### License

BSD License

### Topics

- Tools

### Session SpecCheck

- SpecCheck_Base
- SpecCheck_Generators
- SpecCheck_Show
- SpecCheck_Output_Style
- SpecCheck_Shrink
- SpecCheck
- SpecCheck_Dynamic
- SpecCheck_Examples

### Used by

- Unification Utilities for Isabelle/ML
- Conditional Transfer Rule
- Extension of Types-To-Sets
- Unified Decision Procedures for Regular Expression Equivalence

## Cite

×

SpecCheck-AFP

    @article{SpecCheck-AFP,
      author  = {Kevin Kappelmann and Lukas Bulwahn and Sebastian Willenbrink},
      title   = {SpecCheck - Specification-Based Testing for Isabelle/ML},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/SpecCheck.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Jul 8, 2021 : Isabelle2021