On Tue, 25 May 2010, Yannick Duch�ne (Hibou57) wrote:

> There is a major difference : Eiffel's pre/cond on methods are inherited by
> derived class. With C, or even with Ada' pragma Assert, this have to be done
> manually.
> 
> Side note: I'm not talking about pre/cond in Ada 2012/2015, which will be
> closer to that of Eiffel. However, as SPARK already has this and do it better
> from my point of view (because of static checking and proofs), I am not
> waiting for Ada 2012/2015 for that.

Don't underestmate Ada2012 (or Eiffel, for that point): Being able to 
natively *express* contracts in a programming language itself, instead of 
using some more or less informal comments, as can be done in any other 
languages is a quantum leap. This is regardless of any checking! (Not that 
I disagree with you: Static checking, as provided by SPARK, is a BIG 
THING by itself.)

Defining a derived language which uses the mother language's comments for 
an "annotation" syntax (like SPARK, some Java-derivatives, ...) is the 
poor man's (or poor woman's) approach. I would really hope that SPARK will 
soon after the appearance of Ada 2012 support the new contract syntax.

Stefan

-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------