Re: [isabelle] Unit-Tests for Isabelle Theories



For executable code I do the same thing.

Tobias

On 27/04/2016 14:34, C. Diekmann wrote:
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

2016-04-27 14:18 GMT+02:00 Joachim Breitner <breitner at 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


--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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