Re: GNAT packages in Linux distributions

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 12 May 2010 18:06:16 +0200, Yannick Duchêne (Hibou57) wrote:

> Well, I've noted you do not like runtime-check because it is not [formal]  
> proof of anything, but no one said it is formal proof, this is just better  
> to catch error the sooner and understand why this was an error.

Yes, it is better but that is not the point. Which is there is no
substantial difference between Eiffel precondition and C's if statement
beyond syntax sugar, and that if-statement is less misleading. 

> About expression now, although understandability of a source does not  
> provide proof, this help to at least make partial assertions and discover  
> what's wrong.

No more than an appropriately placed if-statement, tracing call, debugging
break point etc.

> It is best to  
> face an error like “this class invariant was violated” than “this access  
> to this memory address failed”.

The text used in error message is up to the programmer. My objection is not
that what Eiffel offers is useless. The objection is that it has nothing to
do with contracts (in its normal meaning) or with design by. These are no
more than *debugging* tools. Using the terms pre-, postcondition, invariant
is also misleading.

> And like Pascal said : “Eiffel is far more easier than SPARK” (you cannot  
> request every one to know SPARK, and you help them when you provide them  
> something like Eiffel).

Yes, but you do not want to prove everything, which is impossible anyway.
What Ada lacks is better contracts specified by the programmer only when he
wishes to. E,g, exception contracts, statements about purity of a function,
upper bound of stack use etc.

IMO, Ada does not need Eiffel-like pre- postconditions, assertions etc.
They add nothing to safety and thus to Ada. It would be enough to introduce

   raise when <condition>;

and close the theme. (Yes I heard the argument that one can use them in
declarations. I don't think that is a good idea. I don't like exceptions
from declarations.)

Ada had dynamic constraints long before Eiffel. If one wished to extend
this feature, it is welcome. Just do not call it "error check", when you
use the subtype Positive. Tie it to subtypes.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de