On Wed, Sep 26, 2012 at 6:38 PM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
Was checking expressions the only reason they were introduced in the first place?
There were more reasons:
[snip]
2. They (would) provide a standardised description of certain properties of the code that could be used by tools for code analysis or generation. For instance tools could auto-generate unit tests. Or certain optimizations could be performed based on the knowledge contained in axioms.
I was a while back trying to integrate Isabelle/HOL with C and C++ through emacs. It would be really cool if that was possible, and with a standardized syntax for axioms it would be probably easier to interoperate between tools. Though for this task axioms as-is may not be enough for isabelle and comments would still be required.
Regards, &rzej
-- Felipe Magno de Almeida