[isabelle-dev] NEWS: Quickcheck
bulwahn at in.tum.de
Mon Dec 5 13:52:17 CET 2011
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.
More information about the isabelle-dev