src/HOL/Mutabelle/MutabelleExtra.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63167 0909deb8059b
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
executable domain membership checks
bulwahn@34965
     1
theory MutabelleExtra
blanchet@49992
     2
imports Complex_Main "~~/src/HOL/Library/Refute"
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
wenzelm@63167
    18
section \<open>configuration\<close>
bulwahn@34965
    19
wenzelm@63167
    20
ML \<open>val log_directory = ""\<close>
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@56850
    26
nitpick_params [timeout = 5, sat_solver = MiniSat_JNI, 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
*)
bulwahn@34965
    29
wenzelm@63167
    30
ML \<open>val mtds = [
bulwahn@40653
    31
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
bulwahn@40653
    32
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
bulwahn@40653
    33
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
bulwahn@40653
    34
  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"
bulwahn@40653
    35
]
wenzelm@63167
    36
\<close>
bulwahn@40653
    37
wenzelm@63167
    38
ML \<open>
bulwahn@40653
    39
fun mutation_testing_of (name, thy) =
wenzelm@56147
    40
  (MutabelleExtra.init_random 1.0;
bulwahn@40653
    41
  MutabelleExtra.thms_of false thy
bulwahn@40653
    42
  |> MutabelleExtra.take_random 200
bulwahn@40653
    43
  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
bulwahn@46454
    44
         @{theory} (1, 50) mtds thms (log_directory ^ "/" ^ name)))
wenzelm@63167
    45
\<close>
bulwahn@40653
    46
  
bulwahn@34965
    47
wenzelm@63167
    48
text \<open>Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main.\<close>
bulwahn@34965
    49
bulwahn@40653
    50
(*
bulwahn@34965
    51
ML {*
bulwahn@40653
    52
wenzelm@56147
    53
      MutabelleExtra.init_random 1.0;
bulwahn@34965
    54
      MutabelleExtra.thms_of true @{theory Complex_Main}
bulwahn@34965
    55
      |> MutabelleExtra.take_random 1000000
bulwahn@34965
    56
      |> (fn thms => List.drop (thms, 1000))
bulwahn@34965
    57
      |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
bulwahn@40653
    58
             @{theory} [
bulwahn@40653
    59
                        MutabelleExtra.quickcheck_mtd "code",
bulwahn@40653
    60
                        MutabelleExtra.smallcheck_mtd
bulwahn@34965
    61
                        (*MutabelleExtra.refute_mtd,
bulwahn@34965
    62
                        MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
bulwahn@40653
    63
bulwahn@40653
    64
 *}
bulwahn@34965
    65
*)
bulwahn@40653
    66
wenzelm@63167
    67
section \<open>Mutation testing Isabelle theories\<close>
bulwahn@40653
    68
wenzelm@63167
    69
subsection \<open>List theory\<close>
bulwahn@40653
    70
bulwahn@40653
    71
(*
bulwahn@40653
    72
ML {*
bulwahn@40653
    73
mutation_testing_of ("List", @{theory List})
bulwahn@34965
    74
 *}
bulwahn@40653
    75
*)
bulwahn@40653
    76
wenzelm@63167
    77
section \<open>Mutation testing AFP theories\<close>
bulwahn@40653
    78
wenzelm@63167
    79
subsection \<open>AVL-Trees\<close>
bulwahn@40653
    80
bulwahn@40653
    81
(*
bulwahn@40653
    82
ML {*
bulwahn@40653
    83
mutation_testing_of ("AVL-Trees", @{theory AVL})
bulwahn@40653
    84
 *}
bulwahn@40653
    85
*)
bulwahn@40653
    86
wenzelm@63167
    87
subsection \<open>BinaryTree\<close>
bulwahn@40653
    88
bulwahn@40653
    89
(*
bulwahn@40653
    90
ML {*
bulwahn@40653
    91
mutation_testing_of ("BinaryTree", @{theory BinaryTree})
bulwahn@40653
    92
 *}
bulwahn@40653
    93
*)
bulwahn@40653
    94
wenzelm@63167
    95
subsection \<open>Huffman\<close>
bulwahn@40653
    96
bulwahn@40653
    97
(*
bulwahn@40653
    98
ML {*
bulwahn@40653
    99
mutation_testing_of ("Huffman", @{theory Huffman})
bulwahn@40653
   100
 *}
bulwahn@40653
   101
*)
bulwahn@34965
   102
wenzelm@63167
   103
subsection \<open>List_Index\<close>
bulwahn@40653
   104
bulwahn@40653
   105
(*
bulwahn@40653
   106
ML {*
bulwahn@40653
   107
mutation_testing_of ("List_Index", @{theory List_Index})
bulwahn@40653
   108
 *}
bulwahn@40653
   109
*)
bulwahn@40653
   110
wenzelm@63167
   111
subsection \<open>Matrix\<close>
bulwahn@40653
   112
bulwahn@40653
   113
(*
bulwahn@40653
   114
ML {*
bulwahn@40653
   115
mutation_testing_of ("Matrix", @{theory Matrix})
bulwahn@40653
   116
 *}
bulwahn@40653
   117
*)
bulwahn@40653
   118
wenzelm@63167
   119
subsection \<open>NBE\<close>
bulwahn@40653
   120
bulwahn@40653
   121
(*
bulwahn@40653
   122
ML {*
bulwahn@40653
   123
mutation_testing_of ("NBE", @{theory NBE})
bulwahn@40653
   124
 *}
bulwahn@40653
   125
*)
bulwahn@40653
   126
wenzelm@63167
   127
subsection \<open>Polynomial\<close>
bulwahn@40653
   128
bulwahn@40653
   129
(*
bulwahn@40653
   130
ML {*
bulwahn@40653
   131
mutation_testing_of ("Polynomial", @{theory Polynomial})
bulwahn@40653
   132
 *}
bulwahn@40653
   133
*)
bulwahn@40653
   134
wenzelm@63167
   135
subsection \<open>Presburger Automata\<close>
bulwahn@40653
   136
bulwahn@40653
   137
(*
bulwahn@40653
   138
ML {*
bulwahn@40653
   139
mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
bulwahn@40653
   140
 *}
bulwahn@40653
   141
*)
bulwahn@34965
   142
blanchet@39324
   143
end