src/Tools/Spec_Check/README
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 53164 beb4ee344c22
permissions -rw-r--r--
more strict AFP properties;
wenzelm@53164
     1
This is a Quickcheck tool for Isabelle/ML.
bulwahn@52248
     2
bulwahn@52248
     3
Authors
bulwahn@52248
     4
bulwahn@52248
     5
  Lukas Bulwahn
bulwahn@52248
     6
  Nicolai Schaffroth
bulwahn@52248
     7
bulwahn@52248
     8
Quick Usage
bulwahn@52248
     9
bulwahn@52248
    10
  - Import Spec_Check.thy in your development
bulwahn@52248
    11
  - Look at examples in Examples.thy
wenzelm@52260
    12
  - write specifications with the ML invocation
wenzelm@52260
    13
      check_property "ALL x. P x"
bulwahn@52248
    14
bulwahn@52248
    15
Notes
bulwahn@52248
    16
bulwahn@52248
    17
Our specification-based testing tool originated from Christopher League's
bulwahn@52248
    18
QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
bulwahn@52248
    19
provides a rich and uniform ML platform (called Isabelle/ML), this
bulwahn@52248
    20
testing tools is very different than the one for a typical ML developer.
bulwahn@52248
    21
bulwahn@52248
    22
1. Isabelle/ML provides common data structures, which we can use in the
bulwahn@52248
    23
tool's implementation for storing data and printing output.
bulwahn@52248
    24
bulwahn@52248
    25
2. The implementation in Isabelle that will be checked with this tool
bulwahn@52248
    26
commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
bulwahn@52248
    27
but they do not use other integer types in ML, such as ML's Int.int,
bulwahn@52248
    28
Word.word and others.
bulwahn@52248
    29
bulwahn@52248
    30
3. As Isabelle can run heavily in parallel, we avoid reference types.
bulwahn@52248
    31
bulwahn@52248
    32
4. Isabelle has special naming conventions and documentation of source
bulwahn@52248
    33
code is only minimal to avoid parroting.
bulwahn@52248
    34
bulwahn@52248
    35
Next steps:
bulwahn@52248
    36
  - Remove all references and store the neccessary random seed in the
bulwahn@52248
    37
    Isabelle's context.
bulwahn@52248
    38
  - Simplify some existing random generators.
bulwahn@52248
    39
    The original ones from Christopher League are so complicated to
bulwahn@52248
    40
    support many integer types uniformly.
bulwahn@52248
    41
bulwahn@52248
    42
License
bulwahn@52248
    43
bulwahn@52248
    44
  The source code originated from Christopher League's QCheck, which is
bulwahn@52248
    45
  licensed under the 2-clause BSD license. The current source code is
bulwahn@52248
    46
  licensed under the compatible 3-clause BSD license of Isabelle.
bulwahn@52248
    47