[isabelle-dev] Testing the QuickCheck setup
mail at andreas-lochbihler.de
Mon Aug 6 19:37:46 CEST 2018
Testing quickcheck is indeed quite tricky. Do you know which of the quickcheck calls time
out? Does it happen only with the random generator or also with exhaustive?
It might be that you have a fairly large set of code equations and the timeout already
kicks in during code generation or compilation with PolyML, though. A larger timeout
should help there.
Moreover, both statements have two free variables and you rely on the quickcheck
generators being able to quickly come up with two different values for them. If you are
not to set on the property, you could alternatively use
lemma "x ~= x" for x :: dec
which will definitely fail on the first generated example.
Hope this helps,
On 06/08/18 07:57, Lars Hupel wrote:
> Dear list,
> I've been trying to test some QuickCheck generators in the CakeML
> formalization, like so:
> Unfortunately, it seems that they fail occasionally. I've tried
> increasing the timeout, but that still seems to be problematic.
> Is there a way to make these tests more robust? I don't want to comment
> out the checks because much of the QuickCheck setup silently fails if
> something is broken; meaning e.g. that Auto QuickCheck just doesn't work
> on a proposition where it should work.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev