Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Felipe Magno de Almeida (felipe.m.almeida_at_[hidden])
Date: 2012-10-06 10:51:49

On Wed, Sep 26, 2012 at 6:38 PM, Andrzej Krzemienski <akrzemi1_at_[hidden]> 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