src/HOL/Mutabelle/MutabelleExtra.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (23 months ago) changeset 66695 91500c024c7f parent 66453 cc19f7ca2ed6 child 69597 ff784d5a5bfb permissions -rw-r--r--
tuned;
```     1 theory MutabelleExtra
```
```     2 imports 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"*)
```
```    12 begin
```
```    13
```
```    14 ML_file "mutabelle.ML"
```
```    15 ML_file "mutabelle_extra.ML"
```
```    16
```
```    17
```
```    18 section \<open>configuration\<close>
```
```    19
```
```    20 ML \<open>val log_directory = ""\<close>
```
```    21
```
```    22
```
```    23 quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
```
```    24
```
```    25 (*
```
```    26 nitpick_params [timeout = 5, sat_solver = MiniSat_JNI, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
```
```    27 refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
```
```    28 *)
```
```    29
```
```    30 ML \<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
```
```    38 ML \<open>
```
```    39 fun 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
```
```    48 text \<open>Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main.\<close>
```
```    49
```
```    50 (*
```
```    51 ML {*
```
```    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
```
```    67 section \<open>Mutation testing Isabelle theories\<close>
```
```    68
```
```    69 subsection \<open>List theory\<close>
```
```    70
```
```    71 (*
```
```    72 ML {*
```
```    73 mutation_testing_of ("List", @{theory List})
```
```    74  *}
```
```    75 *)
```
```    76
```
```    77 section \<open>Mutation testing AFP theories\<close>
```
```    78
```
```    79 subsection \<open>AVL-Trees\<close>
```
```    80
```
```    81 (*
```
```    82 ML {*
```
```    83 mutation_testing_of ("AVL-Trees", @{theory AVL})
```
```    84  *}
```
```    85 *)
```
```    86
```
```    87 subsection \<open>BinaryTree\<close>
```
```    88
```
```    89 (*
```
```    90 ML {*
```
```    91 mutation_testing_of ("BinaryTree", @{theory BinaryTree})
```
```    92  *}
```
```    93 *)
```
```    94
```
```    95 subsection \<open>Huffman\<close>
```
```    96
```
```    97 (*
```
```    98 ML {*
```
```    99 mutation_testing_of ("Huffman", @{theory Huffman})
```
```   100  *}
```
```   101 *)
```
```   102
```
```   103 subsection \<open>List_Index\<close>
```
```   104
```
```   105 (*
```
```   106 ML {*
```
```   107 mutation_testing_of ("List_Index", @{theory List_Index})
```
```   108  *}
```
```   109 *)
```
```   110
```
```   111 subsection \<open>Matrix\<close>
```
```   112
```
```   113 (*
```
```   114 ML {*
```
```   115 mutation_testing_of ("Matrix", @{theory Matrix})
```
```   116  *}
```
```   117 *)
```
```   118
```
```   119 subsection \<open>NBE\<close>
```
```   120
```
```   121 (*
```
```   122 ML {*
```
```   123 mutation_testing_of ("NBE", @{theory NBE})
```
```   124  *}
```
```   125 *)
```
```   126
```
```   127 subsection \<open>Polynomial\<close>
```
```   128
```
```   129 (*
```
```   130 ML {*
```
```   131 mutation_testing_of ("Polynomial", @{theory Polynomial})
```
```   132  *}
```
```   133 *)
```
```   134
```
```   135 subsection \<open>Presburger Automata\<close>
```
```   136
```
```   137 (*
```
```   138 ML {*
```
```   139 mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
```
```   140  *}
```
```   141 *)
```
```   142
```
```   143 end
```