src/HOL/Mutabelle/MutabelleExtra.thy
changeset 40653 d921c97bdbd8
parent 40341 03156257040f
child 40931 061b8257ab9f
     1.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Nov 22 11:34:58 2010 +0100
     1.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Nov 22 11:34:59 2010 +0100
     1.3 @@ -1,58 +1,144 @@
     1.4  theory MutabelleExtra
     1.5 -imports Complex_Main SML_Quickcheck
     1.6 -(*
     1.7 -  "~/Downloads/Jinja/J/TypeSafe"
     1.8 -  "~/Downloads/Jinja/J/Annotate"
     1.9 -  (* FIXME "Example" *)
    1.10 -  "~/Downloads/Jinja/J/execute_Bigstep"
    1.11 -  "~/Downloads/Jinja/J/execute_WellType"
    1.12 -  "~/Downloads/Jinja/JVM/JVMDefensive"
    1.13 -  "~/Downloads/Jinja/JVM/JVMListExample"
    1.14 -  "~/Downloads/Jinja/BV/BVExec"
    1.15 -  "~/Downloads/Jinja/BV/LBVJVM"
    1.16 -  "~/Downloads/Jinja/BV/BVNoTypeError"
    1.17 -  "~/Downloads/Jinja/BV/BVExample"
    1.18 -  "~/Downloads/Jinja/Compiler/TypeComp"
    1.19 -*)
    1.20 -(*"~/Downloads/NormByEval/NBE"*)
    1.21 -uses "mutabelle.ML"
    1.22 +imports Complex_Main
    1.23 +(*  "~/repos/afp/thys/AVL-Trees/AVL"
    1.24 +  "~/repos/afp/thys/BinarySearchTree/BinaryTree"
    1.25 +  "~/repos/afp/thys/Huffman/Huffman"
    1.26 +  "~/repos/afp/thys/List-Index/List_Index"
    1.27 +  "~/repos/afp/thys/Matrix/Matrix"
    1.28 +  "~/repos/afp/thys/NormByEval/NBE"
    1.29 +  "~/repos/afp/thys/Polynomials/Polynomial"
    1.30 +  "~/repos/afp/thys/Presburger-Automata/Presburger_Automata"
    1.31 +  "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
    1.32 +uses
    1.33 +     "mutabelle.ML"
    1.34       "mutabelle_extra.ML"
    1.35  begin
    1.36  
    1.37 -(* FIXME !?!?! *)
    1.38 -ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
    1.39 -ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
    1.40 -ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
    1.41 -ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
    1.42 +
    1.43 +section {* configuration *}
    1.44  
    1.45 -quickcheck_params [size = 5, iterations = 1000]
    1.46 +ML {* val log_directory = "" *}
    1.47 +
    1.48 +
    1.49 +quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
    1.50 +
    1.51  (*
    1.52  nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
    1.53  refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
    1.54  *)
    1.55  ML {* Auto_Tools.time_limit := 10 *}
    1.56  
    1.57 +ML {* val mtds = [
    1.58 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
    1.59 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
    1.60 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
    1.61 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"
    1.62 +]
    1.63 +*}
    1.64 +
    1.65 +ML {*
    1.66 +fun mutation_testing_of (name, thy) =
    1.67 +  (MutabelleExtra.random_seed := 1.0;
    1.68 +  MutabelleExtra.thms_of false thy
    1.69 +  |> MutabelleExtra.take_random 200
    1.70 +  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
    1.71 +         @{theory} mtds thms (log_directory ^ "/" ^ name)))
    1.72 +*}
    1.73 +  
    1.74  
    1.75  text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
    1.76  
    1.77 +(*
    1.78  ML {*
    1.79 -(*
    1.80 +
    1.81        MutabelleExtra.random_seed := 1.0;
    1.82        MutabelleExtra.thms_of true @{theory Complex_Main}
    1.83        |> MutabelleExtra.take_random 1000000
    1.84        |> (fn thms => List.drop (thms, 1000))
    1.85        |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
    1.86 -             @{theory} [MutabelleExtra.quickcheck_mtd "SML",
    1.87 -                        MutabelleExtra.quickcheck_mtd "code"
    1.88 +             @{theory} [
    1.89 +                        MutabelleExtra.quickcheck_mtd "code",
    1.90 +                        MutabelleExtra.smallcheck_mtd
    1.91                          (*MutabelleExtra.refute_mtd,
    1.92                          MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
    1.93 +
    1.94 + *}
    1.95  *)
    1.96 +
    1.97 +section {* Mutation testing Isabelle theories *}
    1.98 +
    1.99 +subsection {* List theory *}
   1.100 +
   1.101 +(*
   1.102 +ML {*
   1.103 +mutation_testing_of ("List", @{theory List})
   1.104   *}
   1.105 +*)
   1.106 +
   1.107 +section {* Mutation testing AFP theories *}
   1.108 +
   1.109 +subsection {* AVL-Trees *}
   1.110 +
   1.111 +(*
   1.112 +ML {*
   1.113 +mutation_testing_of ("AVL-Trees", @{theory AVL})
   1.114 + *}
   1.115 +*)
   1.116 +
   1.117 +subsection {* BinaryTree *}
   1.118 +
   1.119 +(*
   1.120 +ML {*
   1.121 +mutation_testing_of ("BinaryTree", @{theory BinaryTree})
   1.122 + *}
   1.123 +*)
   1.124 +
   1.125 +subsection {* Huffman *}
   1.126 +
   1.127 +(*
   1.128 +ML {*
   1.129 +mutation_testing_of ("Huffman", @{theory Huffman})
   1.130 + *}
   1.131 +*)
   1.132  
   1.133 -(* FIXME !?!?! *)
   1.134 -ML {* Output.Private_Hooks.tracing_fn := old_tr *}
   1.135 -ML {* Output.Private_Hooks.writeln_fn := old_wr *}
   1.136 -ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
   1.137 -ML {* Output.Private_Hooks.warning_fn := old_wa *}
   1.138 +subsection {* List_Index *}
   1.139 +
   1.140 +(*
   1.141 +ML {*
   1.142 +mutation_testing_of ("List_Index", @{theory List_Index})
   1.143 + *}
   1.144 +*)
   1.145 +
   1.146 +subsection {* Matrix *}
   1.147 +
   1.148 +(*
   1.149 +ML {*
   1.150 +mutation_testing_of ("Matrix", @{theory Matrix})
   1.151 + *}
   1.152 +*)
   1.153 +
   1.154 +subsection {* NBE *}
   1.155 +
   1.156 +(*
   1.157 +ML {*
   1.158 +mutation_testing_of ("NBE", @{theory NBE})
   1.159 + *}
   1.160 +*)
   1.161 +
   1.162 +subsection {* Polynomial *}
   1.163 +
   1.164 +(*
   1.165 +ML {*
   1.166 +mutation_testing_of ("Polynomial", @{theory Polynomial})
   1.167 + *}
   1.168 +*)
   1.169 +
   1.170 +subsection {* Presburger Automata *}
   1.171 +
   1.172 +(*
   1.173 +ML {*
   1.174 +mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
   1.175 + *}
   1.176 +*)
   1.177  
   1.178  end