1theory MutabelleExtra
2imports Complex_Main "HOL-Library.Refute"
3(*  "~/repos/afp/thys/AVL-Trees/AVL"
4  "~/repos/afp/thys/BinarySearchTree/BinaryTree"
5  "~/repos/afp/thys/Huffman/Huffman"
6  "~/repos/afp/thys/List-Index/List_Index"
7  "~/repos/afp/thys/Matrix/Matrix"
8  "~/repos/afp/thys/NormByEval/NBE"
9  "~/repos/afp/thys/Polynomials/Polynomial"
10  "~/repos/afp/thys/Presburger-Automata/Presburger_Automata"
11  "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
12begin
13
14ML_file \<open>mutabelle.ML\<close>
15ML_file \<open>mutabelle_extra.ML\<close>
16
17
18section \<open>configuration\<close>
19
20ML \<open>val log_directory = ""\<close>
21
22
23quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
24
25(*
26nitpick_params [timeout = 5, sat_solver = MiniSat_JNI, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
27refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
28*)
29
30ML \<open>val mtds = [
31  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
32  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
33  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
34  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"
35]
36\<close>
37
38ML \<open>
39fun mutation_testing_of (name, thy) =
40  (MutabelleExtra.init_random 1.0;
41  MutabelleExtra.thms_of false thy
42  |> MutabelleExtra.take_random 200
43  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
44         \<^theory> (1, 50) mtds thms (log_directory ^ "/" ^ name)))
45\<close>
46  
47
48text \<open>Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main.\<close>
49
50(*
51ML {*
52
53      MutabelleExtra.init_random 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
58             @{theory} [
59                        MutabelleExtra.quickcheck_mtd "code",
60                        MutabelleExtra.smallcheck_mtd
61                        (*MutabelleExtra.refute_mtd,
62                        MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
63
64 *}
65*)
66
67section \<open>Mutation testing Isabelle theories\<close>
68
69subsection \<open>List theory\<close>
70
71(*
72ML {*
73mutation_testing_of ("List", @{theory List})
74 *}
75*)
76
77section \<open>Mutation testing AFP theories\<close>
78
79subsection \<open>AVL-Trees\<close>
80
81(*
82ML {*
83mutation_testing_of ("AVL-Trees", @{theory AVL})
84 *}
85*)
86
87subsection \<open>BinaryTree\<close>
88
89(*
90ML {*
91mutation_testing_of ("BinaryTree", @{theory BinaryTree})
92 *}
93*)
94
95subsection \<open>Huffman\<close>
96
97(*
98ML {*
99mutation_testing_of ("Huffman", @{theory Huffman})
100 *}
101*)
102
103subsection \<open>List_Index\<close>
104
105(*
106ML {*
107mutation_testing_of ("List_Index", @{theory List_Index})
108 *}
109*)
110
111subsection \<open>Matrix\<close>
112
113(*
114ML {*
115mutation_testing_of ("Matrix", @{theory Matrix})
116 *}
117*)
118
119subsection \<open>NBE\<close>
120
121(*
122ML {*
123mutation_testing_of ("NBE", @{theory NBE})
124 *}
125*)
126
127subsection \<open>Polynomial\<close>
128
129(*
130ML {*
131mutation_testing_of ("Polynomial", @{theory Polynomial})
132 *}
133*)
134
135subsection \<open>Presburger Automata\<close>
136
137(*
138ML {*
139mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
140 *}
141*)
142
143end
144