Re: [isabelle] quickcheck and error constants

That's a discussion we have been having internally as well. For example, autoquickcheck currently does not object to "hd xs # tl xs = xs" because it ignores the Match exception thrown by "hd []". We'll take this discussion up again (with a reduced audience).


John Matthews schrieb:
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  

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.