src/HOL/Mutabelle/MutabelleExtra.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 56850 13a7bca533a3
child 63167 0909deb8059b
permissions -rw-r--r--
specialized specification: avoid trivial instances
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
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@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
bulwahn@40653
    30
ML {* 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
]
bulwahn@40653
    36
*}
bulwahn@40653
    37
bulwahn@40653
    38
ML {*
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)))
bulwahn@40653
    45
*}
bulwahn@40653
    46
  
bulwahn@34965
    47
bulwahn@34965
    48
text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
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
bulwahn@40653
    67
section {* Mutation testing Isabelle theories *}
bulwahn@40653
    68
bulwahn@40653
    69
subsection {* List theory *}
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
bulwahn@40653
    77
section {* Mutation testing AFP theories *}
bulwahn@40653
    78
bulwahn@40653
    79
subsection {* AVL-Trees *}
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
bulwahn@40653
    87
subsection {* BinaryTree *}
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
bulwahn@40653
    95
subsection {* Huffman *}
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
bulwahn@40653
   103
subsection {* List_Index *}
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
bulwahn@40653
   111
subsection {* Matrix *}
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
bulwahn@40653
   119
subsection {* NBE *}
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
bulwahn@40653
   127
subsection {* Polynomial *}
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
bulwahn@40653
   135
subsection {* Presburger Automata *}
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