src/HOL/Mutabelle/MutabelleExtra.thy
author wenzelm
Wed Aug 22 22:55:41 2012 +0200 (2012-08-22)
changeset 48891 c0eafbd55de3
parent 46454 d72ab6bf6e6d
child 49992 1e68f4701906
permissions -rw-r--r--
prefer ML_file over old uses;
bulwahn@34965
     1
theory MutabelleExtra
bulwahn@40653
     2
imports Complex_Main
bulwahn@40653
     3
(*  "~/repos/afp/thys/AVL-Trees/AVL"
bulwahn@40653
     4
  "~/repos/afp/thys/BinarySearchTree/BinaryTree"
bulwahn@40653
     5
  "~/repos/afp/thys/Huffman/Huffman"
bulwahn@40653
     6
  "~/repos/afp/thys/List-Index/List_Index"
bulwahn@40653
     7
  "~/repos/afp/thys/Matrix/Matrix"
bulwahn@40653
     8
  "~/repos/afp/thys/NormByEval/NBE"
bulwahn@40653
     9
  "~/repos/afp/thys/Polynomials/Polynomial"
bulwahn@40653
    10
  "~/repos/afp/thys/Presburger-Automata/Presburger_Automata"
bulwahn@40653
    11
  "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
bulwahn@34965
    12
begin
bulwahn@34965
    13
wenzelm@48891
    14
ML_file "mutabelle.ML"
wenzelm@48891
    15
ML_file "mutabelle_extra.ML"
wenzelm@48891
    16
bulwahn@40653
    17
bulwahn@40653
    18
section {* configuration *}
bulwahn@34965
    19
bulwahn@40653
    20
ML {* val log_directory = "" *}
bulwahn@40653
    21
bulwahn@40653
    22
bulwahn@40653
    23
quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
bulwahn@40653
    24
bulwahn@34965
    25
(*
blanchet@40341
    26
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
bulwahn@34965
    27
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
bulwahn@34965
    28
*)
blanchet@43018
    29
ML {* Try.auto_time_limit := 10.0 *}
bulwahn@34965
    30
bulwahn@40653
    31
ML {* val mtds = [
bulwahn@40653
    32
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
bulwahn@40653
    33
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
bulwahn@40653
    34
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
bulwahn@40653
    35
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"
bulwahn@40653
    36
]
bulwahn@40653
    37
*}
bulwahn@40653
    38
bulwahn@40653
    39
ML {*
bulwahn@40653
    40
fun mutation_testing_of (name, thy) =
bulwahn@40653
    41
  (MutabelleExtra.random_seed := 1.0;
bulwahn@40653
    42
  MutabelleExtra.thms_of false thy
bulwahn@40653
    43
  |> MutabelleExtra.take_random 200
bulwahn@40653
    44
  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
bulwahn@46454
    45
         @{theory} (1, 50) mtds thms (log_directory ^ "/" ^ name)))
bulwahn@40653
    46
*}
bulwahn@40653
    47
  
bulwahn@34965
    48
bulwahn@34965
    49
text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
bulwahn@34965
    50
bulwahn@40653
    51
(*
bulwahn@34965
    52
ML {*
bulwahn@40653
    53
bulwahn@34965
    54
      MutabelleExtra.random_seed := 1.0;
bulwahn@34965
    55
      MutabelleExtra.thms_of true @{theory Complex_Main}
bulwahn@34965
    56
      |> MutabelleExtra.take_random 1000000
bulwahn@34965
    57
      |> (fn thms => List.drop (thms, 1000))
bulwahn@34965
    58
      |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
bulwahn@40653
    59
             @{theory} [
bulwahn@40653
    60
                        MutabelleExtra.quickcheck_mtd "code",
bulwahn@40653
    61
                        MutabelleExtra.smallcheck_mtd
bulwahn@34965
    62
                        (*MutabelleExtra.refute_mtd,
bulwahn@34965
    63
                        MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
bulwahn@40653
    64
bulwahn@40653
    65
 *}
bulwahn@34965
    66
*)
bulwahn@40653
    67
bulwahn@40653
    68
section {* Mutation testing Isabelle theories *}
bulwahn@40653
    69
bulwahn@40653
    70
subsection {* List theory *}
bulwahn@40653
    71
bulwahn@40653
    72
(*
bulwahn@40653
    73
ML {*
bulwahn@40653
    74
mutation_testing_of ("List", @{theory List})
bulwahn@34965
    75
 *}
bulwahn@40653
    76
*)
bulwahn@40653
    77
bulwahn@40653
    78
section {* Mutation testing AFP theories *}
bulwahn@40653
    79
bulwahn@40653
    80
subsection {* AVL-Trees *}
bulwahn@40653
    81
bulwahn@40653
    82
(*
bulwahn@40653
    83
ML {*
bulwahn@40653
    84
mutation_testing_of ("AVL-Trees", @{theory AVL})
bulwahn@40653
    85
 *}
bulwahn@40653
    86
*)
bulwahn@40653
    87
bulwahn@40653
    88
subsection {* BinaryTree *}
bulwahn@40653
    89
bulwahn@40653
    90
(*
bulwahn@40653
    91
ML {*
bulwahn@40653
    92
mutation_testing_of ("BinaryTree", @{theory BinaryTree})
bulwahn@40653
    93
 *}
bulwahn@40653
    94
*)
bulwahn@40653
    95
bulwahn@40653
    96
subsection {* Huffman *}
bulwahn@40653
    97
bulwahn@40653
    98
(*
bulwahn@40653
    99
ML {*
bulwahn@40653
   100
mutation_testing_of ("Huffman", @{theory Huffman})
bulwahn@40653
   101
 *}
bulwahn@40653
   102
*)
bulwahn@34965
   103
bulwahn@40653
   104
subsection {* List_Index *}
bulwahn@40653
   105
bulwahn@40653
   106
(*
bulwahn@40653
   107
ML {*
bulwahn@40653
   108
mutation_testing_of ("List_Index", @{theory List_Index})
bulwahn@40653
   109
 *}
bulwahn@40653
   110
*)
bulwahn@40653
   111
bulwahn@40653
   112
subsection {* Matrix *}
bulwahn@40653
   113
bulwahn@40653
   114
(*
bulwahn@40653
   115
ML {*
bulwahn@40653
   116
mutation_testing_of ("Matrix", @{theory Matrix})
bulwahn@40653
   117
 *}
bulwahn@40653
   118
*)
bulwahn@40653
   119
bulwahn@40653
   120
subsection {* NBE *}
bulwahn@40653
   121
bulwahn@40653
   122
(*
bulwahn@40653
   123
ML {*
bulwahn@40653
   124
mutation_testing_of ("NBE", @{theory NBE})
bulwahn@40653
   125
 *}
bulwahn@40653
   126
*)
bulwahn@40653
   127
bulwahn@40653
   128
subsection {* Polynomial *}
bulwahn@40653
   129
bulwahn@40653
   130
(*
bulwahn@40653
   131
ML {*
bulwahn@40653
   132
mutation_testing_of ("Polynomial", @{theory Polynomial})
bulwahn@40653
   133
 *}
bulwahn@40653
   134
*)
bulwahn@40653
   135
bulwahn@40653
   136
subsection {* Presburger Automata *}
bulwahn@40653
   137
bulwahn@40653
   138
(*
bulwahn@40653
   139
ML {*
bulwahn@40653
   140
mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
bulwahn@40653
   141
 *}
bulwahn@40653
   142
*)
bulwahn@34965
   143
blanchet@39324
   144
end