[isabelle-dev] NEWS: Quickcheck

Lukas Bulwahn 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 mailing list