Re: [isabelle] quickcheck and error constants

Thanks, Stefan. Is it possible to have a special "undefined" or "quickcheck" exception that is not silently ignored by quickcheck? I want to make cerror executable exactly so that autoquickcheck will tell me if I have an unintended execution path leading to it.


On May 10, 2008, at 2:37 PM, Stefan Berghofer wrote:

Tobias Nipkow wrote:
However, there are two things that puzzle me, that the implementor might
be able to comment on:

1. autoquickcheck does seem to kick in or its result is hidden...

auto quickcheck only outputs something if it finds a counterexample,
i.e. the goal evaluates to False. If the code generator signals an error because the current goal is not executable, the compilation of the generated code fails because it is ill-formed, or an exception is raised during the execution of the code, this is silently ignored. The rationale behind this was to prevent auto quickcheck from displaying too many "spam messages" that
might confuse users.

2. If in the ML code for cerror I replace the i by _, I have a problem:
the generatd ML does not type check...

The problem is that _ has a special meaning: like in mixfix templates,
the _ in a declaration

   f ("...")

indicates a position in the ML code "..." where code for the arguments of f should be inserted (see e.g. the definition of "+" in the Int theory). If you want a _ to occur in the ML code, you have to escape it by writing '_
(like in mixfix templates).


Dr. Stefan Berghofer               E-Mail: berghofe at
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  
