src/Tools/Spec_Check/README

clarified no_zero_devisors: makes only sense in a semiring;
actually turn linorder_semidom into a integral domain

This is a Quickcheck tool for Isabelle/ML.

Authors

  Lukas Bulwahn
  Nicolai Schaffroth

Quick Usage

  - Import Spec_Check.thy in your development
  - Look at examples in Examples.thy
  - write specifications with the ML invocation
      check_property "ALL x. P x"

Notes

Our specification-based testing tool originated from Christopher League's
QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
provides a rich and uniform ML platform (called Isabelle/ML), this
testing tools is very different than the one for a typical ML developer.

1. Isabelle/ML provides common data structures, which we can use in the
tool's implementation for storing data and printing output.

2. The implementation in Isabelle that will be checked with this tool
commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
but they do not use other integer types in ML, such as ML's Int.int,
Word.word and others.

3. As Isabelle can run heavily in parallel, we avoid reference types.

4. Isabelle has special naming conventions and documentation of source
code is only minimal to avoid parroting.

Next steps:
  - Remove all references and store the neccessary random seed in the
    Isabelle's context.
  - Simplify some existing random generators.
    The original ones from Christopher League are so complicated to
    support many integer types uniformly.

License

  The source code originated from Christopher League's QCheck, which is
  licensed under the 2-clause BSD license. The current source code is
  licensed under the compatible 3-clause BSD license of Isabelle.