| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
changing the exhaustive generator signatures;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
quickcheck random can also find potential counterexamples;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 09:35:58 +0100 |
bulwahn |
also potential counterexamples in the simple exhaustive testing in quickcheck
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 09:21:09 +0100 |
bulwahn |
adding a exception-safe term reification step in quickcheck; adding examples
|
file |
diff |
annotate
|
| Wed, 30 Nov 2011 09:21:07 +0100 |
bulwahn |
quickcheck returns counterexamples that are potentially spurious due to underspecified code equations and match exceptions
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 11:14:06 +0100 |
bulwahn |
setting up exhaustive generators which are used for the smart generators
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 11:35:09 +0100 |
bulwahn |
more precise messages with the tester's name in quickcheck; tuned
|
file |
diff |
annotate
|
| Mon, 17 Oct 2011 10:19:01 +0200 |
bulwahn |
moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
removing generator registration
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
parametrized test_term functions in quickcheck
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adding random, exhaustive and SML quickcheck as testers
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 09:10:23 +0200 |
bulwahn |
adding bounded_forall tester
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 09:10:23 +0200 |
bulwahn |
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2011 15:00:23 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
correcting constant name in exhaustive_generators
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
switching fast compilation off by default for now in exhaustive quickcheck
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
splitting exhaustive and full_exhaustive into separate type classes
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
removing duplicate code
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
creating a general mk_equation_terms for the different compilations
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
adding an even faster compilation scheme
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:31:14 +0200 |
bulwahn |
new compilation for exhaustive quickcheck
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 14:51:25 +0200 |
bulwahn |
correcting bounded_forall construction; tuned
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 09:38:23 +0200 |
bulwahn |
deriving bounded_forall instances in quickcheck_exhaustive
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 08:53:52 +0200 |
bulwahn |
generalizing ensure_sort_datatype for bounded_forall instances
|
file |
diff |
annotate
|
| Mon, 04 Apr 2011 14:44:11 +0200 |
bulwahn |
refactoring generator definition in quickcheck and removing clone
|
file |
diff |
annotate
|
| Fri, 01 Apr 2011 13:49:38 +0200 |
bulwahn |
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 19:09:57 +0200 |
bulwahn |
removing dead code in exhaustive_generators
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 09:44:16 +0200 |
bulwahn |
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
extending the test data generators to take the evaluation terms as arguments
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 12:34:12 +0100 |
bulwahn |
tuned exhaustive_generators
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 12:34:10 +0100 |
bulwahn |
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
adaptions in generators using the common functions
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
renaming signatures and structures; correcting header
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 15:21:13 +0100 |
bulwahn |
moving exhaustive_generators.ML to Quickcheck directory
|
file |
diff |
annotate
| base
|