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