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