Re: [isabelle] Unit-Tests for Isabelle Theories



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
>
>



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