I am pleased to announce the first public release of DBC for C - a C  
preprocessor that generates contract testing code and documentation  
from DBC tags embedded in C comments.  Here is an example:
/**
   pre: i >= 0
   pre: i < array->length
   post: array->array[i] == elem
  */
void
Array_put(T array, long i, void *elem)
{
   array->array[i] = elem;
}

DBC for C supports preconditions, postconditions, invariants and some  
iterating operators (forall, exists).  Also DBC for C can generate  
Doxygen documentation from contracts.  For more information take a look  
at this article:
http://www.onlamp.com/pub/a/onlamp/2004/10/28/ 
design_by_contract_in_c.html
(also featured on the front page of onlamp.com :)

Project Wiki:
http://dbc.rubyforge.org/wiki/wiki.pl
Download page:
http://rubyforge.org/frs/?group_id=354

The DBC for C source package contains an example library, found in the  
test_app directory.

DBC for C was created with Ruby and Racc.

Many thanks to Marcel Molina Jr. for proof reading the article, Daniel  
Berger for submitting the first bug report, and Dave Thomas for writing  
the book that got this started.

Enjoy!

-Charlie

PS.  Feed back is welcome.