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: > >>Hello all, >> >>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:
Hello all, 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. Greetings, Stefan -- 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
