author | wenzelm |
Mon, 25 Feb 2013 12:17:50 +0100 | |
changeset 51272 | 9c8d63b4b6be |
parent 48179 | 18461f745b4a |
child 58148 | 9764b994a421 |
permissions | -rw-r--r-- |
48179
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
1 |
theory Quickcheck_Interfaces |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
2 |
imports Main |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
3 |
begin |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
4 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
5 |
subsection {* Checking a single proposition (TODO) *} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
6 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
7 |
subsection {* Checking multiple propositions in one batch *} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
8 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
9 |
text {* |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
10 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
11 |
First, this requires to setup special generators for all datatypes via the following command. |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
12 |
*} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
13 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
14 |
setup {* Exhaustive_Generators.setup_bounded_forall_datatype_interpretation *} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
15 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
16 |
text {* |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
17 |
Now, the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (int -> bool) list option |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
18 |
takes formulas of type bool with free variables, and returns a list of testing functions. |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
19 |
*} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
20 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
21 |
ML {* |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
22 |
val SOME testers = Quickcheck.mk_batch_validator @{context} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
23 |
[@{term "x = (1 :: nat)"}, @{term "x = (0 :: nat)"}, @{term "x <= (5 :: nat)"}, @{term "0 \<le> (x :: nat)"}] |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
24 |
*} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
25 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
26 |
text {* |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
27 |
It is upto the user with which strategy the conjectures should be tested. |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
28 |
For example, one could check all conjectures up to a given size, and check the different conjectures in sequence. |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
29 |
This is implemented by: |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
30 |
*} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
31 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
32 |
ML {* |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
33 |
fun check_upto f i j = if i > j then true else f i andalso check_upto f (i + 1) j |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
34 |
*} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
35 |
|
51272 | 36 |
ML_val {* |
48179
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
37 |
map (fn test => check_upto test 0 1) testers |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
38 |
*} |
51272 | 39 |
ML_val {* |
48179
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
40 |
map (fn test => check_upto test 0 2) testers |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
41 |
*} |
51272 | 42 |
ML_val {* |
48179
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
43 |
map (fn test => check_upto test 0 3) testers |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
44 |
*} |
51272 | 45 |
ML_val {* |
48179
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
46 |
map (fn test => check_upto test 0 7) testers |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
47 |
*} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
48 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
49 |
text {* Note that all conjectures must be executable to obtain the testers with the function above. *} |
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
50 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
51 |
|
18461f745b4a
adding some minimal documentation and an example of quickcheck's interfaces
bulwahn
parents:
diff
changeset
|
52 |
end |