| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Quickcheck_Examples/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle Quickcheck_Interfaces.thy Sprache: Isabelle |
|||||||||||||||
|
theory Quickcheck_Interfaces imports Main begin subsection ‹Checking a single proposition (TODO)› subsection ‹Checking multiple propositions in one batch› text ‹ , this requires to setup special generators for all datatypes via the following setup Exhaustive_Generators.setup_bounded_forall_datatype_interpretation text ‹ , the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (in formulas of type bool with free variables, and returns a list of testing functi ML ‹ SOME testers = Quickcheck.mk_batch_validator context [term‹x = (1 :: nat)›, term‹x = (0 :: nat)›, term‹x <= (5 :: nat)›, term‹0 ≤ (x :: › text ‹ is up to the user with which strategy the conjectures should be tested. example, one could check all conjectures up to a given size, and check the diff is implemented by: ML ‹ check_upto f i j = if i > j then true else f i andalso check_upto f (i + 1) j › ML_val ‹ map (fn test => check_upto test 0 1) testers › ML_val ‹ map (fn test => check_upto test 0 2) testers › ML_val ‹ map (fn test => check_upto test 0 3) testers › ML_val ‹ map (fn test => check_upto test 0 7) testers › text ‹Note that all conjectures must be executable to obtain the testers with the end
¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet am 2026-09-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-10-09