26 Sep
2012
26 Sep
'12
9:47 p.m.
On Wed, Sep 26, 2012 at 2:38 PM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
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.
This is true for pre/post/inv as well.
Or certain optimizations could be performed based on the knowledge contained in axioms.
*In theory*, this is also true for pre/pot/inv. P.S. I just wanted to point out similar properties of contracts but I'm not sure if comments I made in this email are relevant for the axiom discussion. --Lorenzo