Re: [isabelle] Unit-Tests for Isabelle Theories


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


2016-04-27 14:18 GMT+02:00 Joachim Breitner <breitner at>:

> 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:
> --
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter

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