Email Gateway (Aug 18 2022 at 20:14): Email Gateway (Aug 18 2022 at 20:14):From: Moa Johansson <moa.johansson@chalmers.se>
Hi,
I'm currently updating IsaPlanner and IsaCoSy to Isabelle2012. Both systems make use of Isabelle's counterexample checker quickcheck, which has been updated. I need to send lists of things of type term for testing, so I'm assuming I need to use the test_term function, which has type
Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option
I'd like to know what the last argument of type (term * term list) list is representing? Which list is the list of terms I want to counter-example check, and what does the first term in the pair represent?
Best,
Moa
Email Gateway (Aug 18 2022 at 20:15):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Looking at the code, it would seem that the first component is _the_ term to check and the second component is a list of terms that are additionally evaluated. For example, if you pass ("rev xs = xs", ["rev xs"]), Quickcheck will find a counterexample and print the value of "rev xs" (in addition to that of "xs"). In your use scenario, you would probably pass an empty list for the second components.
Jasmin
Email Gateway (Aug 18 2022 at 20:15):From: Thomas Genet <thomas.genet@irisa.fr>
Hi to you all.
By the way, it seems that this nice feature of Quickcheck (the "eval"
parameter) does not always work with the narrowing tester. This is not
fully surprising since the narrowing-driven testing may send back
partially instanciated values, like _#[] for instance.
However, if it is the case it may be a good idea to mention this in the
isar manual.
Best regards,
Thomas
Email Gateway (Aug 18 2022 at 20:15):From: Lukas Bulwahn <bulwahn@in.tum.de>
Thanks, Jasmin, for answering this question. The implementation seems to
be self-explanatory, if you could grasp it with one look in the code.
Lukas
Email Gateway (Aug 18 2022 at 20:15):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hi Thomas,
Thanks for this suggestion. I mentioned it in the NEWS file
- Added "eval" option to evaluate terms for the found counterexample
(currently only supported by the default (exhaustive) tester).
but left it out of the Isar reference. A remark has now been added.
It is another technical challenge to enable the eval feature also for
the narrowing tester, and cannot just be dealt with by reusing the
source code for the exhaustive testing infrastructure. Maybe I find time
to add it, maybe not--it's on my TODO list.
Lukas
Last updated: Apr 26 2024 at 08:19 UTC