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
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
because the current goal is not executable, the compilation of the
code fails because it is ill-formed, or an exception is raised
execution of the code, this is silently ignored. The rationale
was to prevent auto quickcheck from displaying too many "spam
might confuse users.
2. If in the ML code for cerror I replace the i by _, I have a
the generatd ML does not type check...
The problem is that _ has a special meaning: like in mixfix templates,
the _ in a declaration
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
you want a _ to occur in the ML code, you have to escape it by
(like in mixfix templates).
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and