Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Isabelle/HOL/Mutabelle/ (Isabelle Prover Version 2025-1^©) Datei vom 16.11.2025 mit Größe 3 kB

Quelle MutabelleExtra.thy

Sprache: Isabelle

theory MutabelleExtra
imports Complex_Main "HOL-Library.Refute"
(*  "~/repos/afp/thys/AVL-Trees/AVL"
  "~/repos/afp/thys/BinarySearchTree/BinaryTree"
  "~/repos/afp/thys/Huffman/Huffman"
  "~/repos/afp/thys/List-Index/List_Index"
  "~/repos/afp/thys/Matrix/Matrix"
  "~/repos/afp/thys/NormByEval/NBE"
  "~/repos/afp/thys/Polynomials/Polynomial"
  "~/repos/afp/thys/Presburger-Automata/Presburger_Automata"
  "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
begin

ML_file ‹mutabelle.ML›
ML_file ‹mutabelle_extra.ML›

section ‹configuration›

ML ‹val log_directory = ""›

quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]

(*
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
*)

ML ‹val mtds = [
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"

›

ML ‹
mutation_testing_of (name, thy) =
(MutabelleExtra.init_random 1.0;
MutabelleExtra.thms_of false thy
|> MutabelleExtra.take_random 200
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
🚫 (1, 50) mtds thms (log_directory ^ "/" ^ name)))
›


text ‹Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main.›

(*
ML {*

      MutabelleExtra.init_random 1.0;
      MutabelleExtra.thms_of true @{theory Complex_Main}
      |> MutabelleExtra.take_random 1000000
      |> (fn thms => List.drop (thms, 1000))
      |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
             @{theory} [
                        MutabelleExtra.quickcheck_mtd "code",
                        MutabelleExtra.smallcheck_mtd
                        (*MutabelleExtra.refute_mtd,
                        MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")

*}
*)

section ‹Mutation testing Isabelle theories›

subsection ‹List theory›

(*
ML {*
mutation_testing_of ("List", @{theory List})
*}
*)

section ‹Mutation testing AFP theories›

subsection ‹AVL-Trees›

(*
ML {*
mutation_testing_of ("AVL-Trees", @{theory AVL})
*}
*)

subsection ‹BinaryTree›

(*
ML {*
mutation_testing_of ("BinaryTree", @{theory BinaryTree})
*}
*)

subsection ‹Huffman›

(*
ML {*
mutation_testing_of ("Huffman", @{theory Huffman})
*}
*)

subsection ‹List_Index›

(*
ML {*
mutation_testing_of ("List_Index", @{theory List_Index})
*}
*)

subsection ‹Matrix›

(*
ML {*
mutation_testing_of ("Matrix", @{theory Matrix})
*}
*)

subsection ‹NBE›

(*
ML {*
mutation_testing_of ("NBE", @{theory NBE})
*}
*)

subsection ‹Polynomial›

(*
ML {*
mutation_testing_of ("Polynomial", @{theory Polynomial})
*}
*)

subsection ‹Presburger Automata›

(*
ML {*
mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
*}
*)

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-06-30) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.