| Thu, 14 Feb 2013 15:27:10 +0100 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 08:17:47 +0100 |
haftmann |
explicit references avoid dynamic lookup
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 20:04:59 +0100 |
haftmann |
note to eliminate dynamic name reference
|
file |
diff |
annotate
|
| Sun, 11 Nov 2012 19:56:02 +0100 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
| Mon, 20 Feb 2012 12:37:17 +0100 |
huffman |
use qualified constant names instead of suffixes (from Florian Haftmann)
|
file |
diff |
annotate
|
| Wed, 25 Jan 2012 15:19:04 +0100 |
bulwahn |
generalizing check if size matters because it is different for random and exhaustive testing
|
file |
diff |
annotate
|
| Wed, 21 Dec 2011 09:21:35 +0100 |
bulwahn |
quickcheck_generator command also creates random generators
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 17:22:31 +0100 |
bulwahn |
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:20 +0100 |
bulwahn |
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:19 +0100 |
bulwahn |
the reporting random testing also returns if the counterexample is genuine or potentially spurious
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:06 +0100 |
bulwahn |
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:03 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:00 +0100 |
bulwahn |
renaming potential flag to genuine_only flag with an inverse semantics
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:35:05 +0100 |
bulwahn |
dynamic genuine_flag in compilation of random and exhaustive
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
compilations return genuine flag to quickcheck framework
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
reporting random compilation also catches match exceptions internally
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
quickcheck-random compilation also indicates if the counterexample is potentially spurious or not
|
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 |
removing exception handling now that is caught at some other point;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
quickcheck random can also find potential counterexamples;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 21:18:38 +0100 |
wenzelm |
added ML antiquotation @{attributes};
|
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
|
| Thu, 09 Jun 2011 23:12:02 +0200 |
wenzelm |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|