[isabelle-dev] quickcheck on type real
berghofe at in.tum.de
Thu Sep 6 17:31:37 CEST 2007
Amine Chaieb wrote:
> This is perhaps an occasion to advertise Library/Executable_real.thy,
> which contains a verified implementation of rational numbers to be have
> like HOL --- So here you would no get an exception when dividing by
> zero, but just zero as you expect.
> Brian Huffman wrote:
>>I would like to report some bugs I found when using quickcheck on lemmas
>>involving division on reals. When auto_quickcheck is enabled (which it is by
>>default) these bugs cause the "lemma" command to fail, preventing me from
>>even attempting a proof.
>>The first bug is that sometimes quickcheck fails with a DIVZERO exception.
>>The other bug is a false counterexample; I have no idea what causes it:
the code generator setup contained in the theories Library/Executable_Real.thy
and Library/Executable_Rat.thy have now been integrated into the theories
Real/RealDef.thy and Real/Rational.thy. Moreover, I modified the setup in such
a way that it also works with the "old" code generator and therefore with
quickcheck, so the abovementioned bugs should now be fixed.
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3 Room: 01.11.059
85748 Garching, GERMANY http://www.in.tum.de/~berghofe
More information about the isabelle-dev