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 command.
›

setup Exhaustive_Generators.setup_bounded_forall_datatype_interpretation

text ‹
, the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
formulas of type bool with free variables, and returns a list of testing functions.
›

ML ‹
SOME testers = Quickcheck.mk_batch_validator 🍋
[term‹x = (1 :: nat)›, term‹x = (0 :: nat)›, term‹x <= (5 :: nat)›, term‹0 ≤ (x :: nat)›]
›

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 different conjectures in sequence.
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 => <>1
›
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 function above.›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.