src/HOL/Mutabelle/MutabelleExtra.thy
author blanchet
Fri May 27 10:30:08 2011 +0200 (2011-05-27)
changeset 43018 121aa59b4d17
parent 40931 061b8257ab9f
child 46453 9e83b7c24b05
permissions -rw-r--r--
renamed "Auto_Tools" "Try"
     1 theory MutabelleExtra
     2 imports Complex_Main
     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 uses
    13      "mutabelle.ML"
    14      "mutabelle_extra.ML"
    15 begin
    16 
    17 
    18 section {* configuration *}
    19 
    20 ML {* val log_directory = "" *}
    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, 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 ML {* Try.auto_time_limit := 10.0 *}
    30 
    31 ML {* val mtds = [
    32   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
    33   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
    34   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
    35   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"
    36 ]
    37 *}
    38 
    39 ML {*
    40 fun mutation_testing_of (name, thy) =
    41   (MutabelleExtra.random_seed := 1.0;
    42   MutabelleExtra.thms_of false thy
    43   |> MutabelleExtra.take_random 200
    44   |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
    45          @{theory} mtds thms (log_directory ^ "/" ^ name)))
    46 *}
    47   
    48 
    49 text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
    50 
    51 (*
    52 ML {*
    53 
    54       MutabelleExtra.random_seed := 1.0;
    55       MutabelleExtra.thms_of true @{theory Complex_Main}
    56       |> MutabelleExtra.take_random 1000000
    57       |> (fn thms => List.drop (thms, 1000))
    58       |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
    59              @{theory} [
    60                         MutabelleExtra.quickcheck_mtd "code",
    61                         MutabelleExtra.smallcheck_mtd
    62                         (*MutabelleExtra.refute_mtd,
    63                         MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
    64 
    65  *}
    66 *)
    67 
    68 section {* Mutation testing Isabelle theories *}
    69 
    70 subsection {* List theory *}
    71 
    72 (*
    73 ML {*
    74 mutation_testing_of ("List", @{theory List})
    75  *}
    76 *)
    77 
    78 section {* Mutation testing AFP theories *}
    79 
    80 subsection {* AVL-Trees *}
    81 
    82 (*
    83 ML {*
    84 mutation_testing_of ("AVL-Trees", @{theory AVL})
    85  *}
    86 *)
    87 
    88 subsection {* BinaryTree *}
    89 
    90 (*
    91 ML {*
    92 mutation_testing_of ("BinaryTree", @{theory BinaryTree})
    93  *}
    94 *)
    95 
    96 subsection {* Huffman *}
    97 
    98 (*
    99 ML {*
   100 mutation_testing_of ("Huffman", @{theory Huffman})
   101  *}
   102 *)
   103 
   104 subsection {* List_Index *}
   105 
   106 (*
   107 ML {*
   108 mutation_testing_of ("List_Index", @{theory List_Index})
   109  *}
   110 *)
   111 
   112 subsection {* Matrix *}
   113 
   114 (*
   115 ML {*
   116 mutation_testing_of ("Matrix", @{theory Matrix})
   117  *}
   118 *)
   119 
   120 subsection {* NBE *}
   121 
   122 (*
   123 ML {*
   124 mutation_testing_of ("NBE", @{theory NBE})
   125  *}
   126 *)
   127 
   128 subsection {* Polynomial *}
   129 
   130 (*
   131 ML {*
   132 mutation_testing_of ("Polynomial", @{theory Polynomial})
   133  *}
   134 *)
   135 
   136 subsection {* Presburger Automata *}
   137 
   138 (*
   139 ML {*
   140 mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
   141  *}
   142 *)
   143 
   144 end