Dear Lars,
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,
Andreas
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:
<https://bitbucket.org/isa-afp/afp-devel/commits/c9f0f80df2108eb2772c6b9492e913f9236613db>
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.
Cheers
Lars
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
