From: Charles Mills <cmills@...>
Date: 2004-12-04T05:54:03+09:00
Subject: Re: [ANN] DBC for C 1.3.0 released

On Dec 3, 2004, at 9:29 AM, Henrik Horneber wrote:

> Friedrich Dominicus wrote:
>
>> Charles Mills <cmills@freeshell.org> writes:
>>> This is a very high quality release thanks to Sebastian Hunt and 
>>> Marc Verwerft. DBC for C now has exceptional GCC support (including 
>>> GCC extensions) and is significantly quicker and more polished than 
>>> the initial releases. (Also has Windows support as of 1.2.3.)
>> good idea but what's the difference to GEF?
>> http://home.rochester.rr.com/bigbyofrocny/GEF/GEF.html
>
GEF uses the C preprocessor.  DBC for C is a preprocessor.  I tried 
using GEF (before I began working on DBC for C) and found it too 
complicated to use.  DBC for C is pretty simple - all you need to do is 
define a function/macro - dbc_error(const char *msg) - which gets 
called whenever a contract condition is not met.  See this article:
http://www.codegeneration.net/tiki-read_article.php?articleId=72
or the wiki (dbc.rubyforge.org) for more info.

One nice thing about DBC for C is it is easy to inject into existing 
project or remove if it doesn't meet your needs.  You can compile the 
code normally or with contract checks in place... add invariants that 
will be checked in through out your project... if it sounds interesting 
I encourage you to check out the links above.  Also there is a pretty 
active mailing list for DBC for C here:
http://rubyforge.org/mail/?group_id=354

> As far as I understand it, DBC for C uses comments in the header file 
> to genrarte contract checking code, whereas GEF hides the contracts 
> specification in the implementation.
>
That's right.... header files and .c files.  Most of the DBC comment 
will be in .c files, especially if you use opaque types.
With GEF contract specifications are part of your function and are 
manipulated using preprocessor macros.

-Charlie