Eine aufbereitete Darstellung der Quelle

 
     
 
 
Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

Benutzer

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 context
 [termx = (1 :: nat), termx = (0 :: nat), termx <= (5 :: nat), term0 (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 => 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 function above.


end

Messung V0.5 in Prozent
C=27 H=64 G=48

¤ Dauer der Verarbeitung: 0.10 Sekunden  (vorverarbeitet am  2026-06-29) ¤

*© Formatika GbR, Deutschland






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.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.






                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Quellcodebibliothek
     Eigene Quellcodes
     Fremde Quellcodes
     Suchen

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik