1 This is a Quickcheck tool for Isabelle's ML environment. |
|
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 |
|