author | wenzelm |
Mon, 29 Jul 2013 19:55:38 +0200 | |
changeset 52776 | fd81d51460b7 |
parent 52639 | df830310e550 |
child 56147 | 9589605bcf41 |
permissions | -rw-r--r-- |
34965 | 1 |
theory MutabelleExtra |
49992 | 2 |
imports Complex_Main "~~/src/HOL/Library/Refute" |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
3 |
(* "~/repos/afp/thys/AVL-Trees/AVL" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
4 |
"~/repos/afp/thys/BinarySearchTree/BinaryTree" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
5 |
"~/repos/afp/thys/Huffman/Huffman" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
6 |
"~/repos/afp/thys/List-Index/List_Index" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
7 |
"~/repos/afp/thys/Matrix/Matrix" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
8 |
"~/repos/afp/thys/NormByEval/NBE" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
9 |
"~/repos/afp/thys/Polynomials/Polynomial" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
10 |
"~/repos/afp/thys/Presburger-Automata/Presburger_Automata" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
11 |
"~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*) |
34965 | 12 |
begin |
13 |
||
48891 | 14 |
ML_file "mutabelle.ML" |
15 |
ML_file "mutabelle_extra.ML" |
|
16 |
||
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
17 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
18 |
section {* configuration *} |
34965 | 19 |
|
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
20 |
ML {* val log_directory = "" *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
21 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
22 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
23 |
quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000] |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
24 |
|
34965 | 25 |
(* |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40133
diff
changeset
|
26 |
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12] |
34965 | 27 |
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat] |
28 |
*) |
|
29 |
||
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
30 |
ML {* val mtds = [ |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
31 |
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random", |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
32 |
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random", |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
33 |
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small", |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
34 |
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small" |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
35 |
] |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
36 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
37 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
38 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
39 |
fun mutation_testing_of (name, thy) = |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
40 |
(MutabelleExtra.random_seed := 1.0; |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
41 |
MutabelleExtra.thms_of false thy |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
42 |
|> MutabelleExtra.take_random 200 |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
43 |
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report |
46454
d72ab6bf6e6d
making num_mutations a configuration that can be changed with the mutabelle bash command
bulwahn
parents:
46453
diff
changeset
|
44 |
@{theory} (1, 50) mtds thms (log_directory ^ "/" ^ name))) |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
45 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
46 |
|
34965 | 47 |
|
48 |
text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *} |
|
49 |
||
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
50 |
(* |
34965 | 51 |
ML {* |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
52 |
|
34965 | 53 |
MutabelleExtra.random_seed := 1.0; |
54 |
MutabelleExtra.thms_of true @{theory Complex_Main} |
|
55 |
|> MutabelleExtra.take_random 1000000 |
|
56 |
|> (fn thms => List.drop (thms, 1000)) |
|
57 |
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report |
|
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
58 |
@{theory} [ |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
59 |
MutabelleExtra.quickcheck_mtd "code", |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
60 |
MutabelleExtra.smallcheck_mtd |
34965 | 61 |
(*MutabelleExtra.refute_mtd, |
62 |
MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out") |
|
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
63 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
64 |
*} |
34965 | 65 |
*) |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
66 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
67 |
section {* Mutation testing Isabelle theories *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
68 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
69 |
subsection {* List theory *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
70 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
71 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
72 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
73 |
mutation_testing_of ("List", @{theory List}) |
34965 | 74 |
*} |
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
75 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
76 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
77 |
section {* Mutation testing AFP theories *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
78 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
79 |
subsection {* AVL-Trees *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
80 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
81 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
82 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
83 |
mutation_testing_of ("AVL-Trees", @{theory AVL}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
84 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
85 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
86 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
87 |
subsection {* BinaryTree *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
88 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
89 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
90 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
91 |
mutation_testing_of ("BinaryTree", @{theory BinaryTree}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
92 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
93 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
94 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
95 |
subsection {* Huffman *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
96 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
97 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
98 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
99 |
mutation_testing_of ("Huffman", @{theory Huffman}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
100 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
101 |
*) |
34965 | 102 |
|
40653
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
103 |
subsection {* List_Index *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
104 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
105 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
106 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
107 |
mutation_testing_of ("List_Index", @{theory List_Index}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
108 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
109 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
110 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
111 |
subsection {* Matrix *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
112 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
113 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
114 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
115 |
mutation_testing_of ("Matrix", @{theory Matrix}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
116 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
117 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
118 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
119 |
subsection {* NBE *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
120 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
121 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
122 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
123 |
mutation_testing_of ("NBE", @{theory NBE}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
124 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
125 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
126 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
127 |
subsection {* Polynomial *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
128 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
129 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
130 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
131 |
mutation_testing_of ("Polynomial", @{theory Polynomial}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
132 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
133 |
*) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
134 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
135 |
subsection {* Presburger Automata *} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
136 |
|
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
137 |
(* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
138 |
ML {* |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
139 |
mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata}) |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
140 |
*} |
d921c97bdbd8
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
bulwahn
parents:
40341
diff
changeset
|
141 |
*) |
34965 | 142 |
|
39324
05452dd66b2b
finished renaming "Auto_Counterexample" to "Auto_Tools"
blanchet
parents:
34965
diff
changeset
|
143 |
end |