--- a/NEWS Mon Dec 05 12:36:02 2011 +0100
+++ b/NEWS Mon Dec 05 12:36:03 2011 +0100
@@ -145,6 +145,21 @@
produces a rule which can be used to perform case distinction on both
a list and a nat.
+* Quickcheck:
+ - Quickcheck returns variable assignments as counterexamples, which
+ allows to reveal the underspecification of functions under test.
+ For example, refuting "hd xs = x", it presents the variable
+ assignment xs = [] and x = a1 as a counterexample, assuming that
+ any property is false whenever "hd []" occurs in it.
+ These counterexample are marked as potentially spurious, as
+ Quickcheck also returns "xs = []" as a counterexample to the
+ obvious theorem "hd xs = hd xs".
+ After finding a potentially spurious counterexample, Quickcheck
+ continues searching for genuine ones.
+ By default, Quickcheck shows potentially spurious and genuine
+ counterexamples. The option "genuine_only" sets quickcheck to
+ only show genuine counterexamples.
+
* Nitpick:
- Fixed infinite loop caused by the 'peephole_optim' option and
affecting 'rat' and 'real'.
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Dec 05 12:36:02 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Dec 05 12:36:03 2011 +0100
@@ -372,8 +372,9 @@
val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_generator_expr,
- absdummy @{typ code_numeral} @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"}),
- @{typ "code_numeral => Random.seed => (bool * term list) option * Random.seed"})
+ absdummy @{typ bool} (absdummy @{typ code_numeral}
+ @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"})),
+ @{typ "bool => code_numeral => Random.seed => (bool * term list) option * Random.seed"})
val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_reporting_generator_expr,