src/HOL/Mutabelle/MutabelleExtra.thy
author wenzelm
Thu May 26 17:51:22 2016 +0200 (2016-05-26)
changeset 63167 0909deb8059b
parent 56850 13a7bca533a3
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     1 theory MutabelleExtra
     2 imports Complex_Main "~~/src/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