Boost logo

Boost :

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:


> 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

Boost list run by bdawes at, gregod at, cpdaniel at, john at