Email Gateway (Aug 22 2022 at 13:13): Email Gateway (Aug 22 2022 at 13:13):From: Joachim Breitner <breitner@kit.edu>
Dear list,
in the context of our Isabelle course in Karlsruhe we are wondering
what solutions exists (or should exist) to the question:
How do you test Isabelle theories?
I know that we usually position proving as a (better) alternative to
testing. But even our Isabelle theories are, in a certain sense, code:
They provide functionality behind a certain interface (lemmas with
certain names capable to prove certain facts; simplifier setups that
are supposed to solve certain classes of questions). With that view in
mind, testing procedures from software development might make sense in
our setting as well!
More concretely: What is the most reliable and convenient way of
automatically¹ asserting that a certain Isabelle theory correctly
implements certain functionality?
Thanks for your input,
Joachim Breitner
¹ Our students submit their Isabelle theories via the Praktomat, which
has support for running Isabelle theories in a confined docker
contianer: http://pp.ipd.kit.edu/projects/praktomat/praktomat.php
signature.asc
Email Gateway (Aug 22 2022 at 13:13):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
I do some very inefficient quick'n'dirty unit testing on my algorithms
directly in the thy files:
lemma "code input = expected_result" by eval
Best,
Cornelius
Email Gateway (Aug 22 2022 at 13:13):From: Tobias Nipkow <nipkow@in.tum.de>
For executable code I do the same thing.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 13:13):From: Thomas Sewell <thomas.sewell@nicta.com.au>
You could "test" the formal environment created by testing the
effectiveness of the automatic methods (simplifier, auto, sledgehammer)
once the theory is loaded.
Of course, that requires a collection of hypotheses about the relevant
constants. It's not clear where that would come from for original
theories. For theories which match a development in some other logic or
textbook, you could do comparisons.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 19 2024 at 08:19 UTC