Re: GNAT packages in Linux distributions

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

On Wed, 12 May 2010 20:09:49 +0200, Georg Bauhaus wrote:

> On 12.05.10 19:24, Dmitry A. Kazakov wrote:
>> 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.
> 
> Being better is precisely the point (of DbC).
> DbC talks about proof obligations, not about provability.

Who is obliged to whom in what?

>> there is no
>> substantial difference between Eiffel precondition and C's if statement
>> beyond syntax sugar, and that if-statement is less misleading. 
> 
> "If" is
> - much more flexible and
> - totally unspecific and
> - not integrated with, e.g. rescue clauses;
> - needs bodies
> 
> You can emulate anything with "if" or write assembler, though ... .

Yes, but all above is not substantial.

>>> 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.
> 
> You cannot place an "if" in a specification.

The answer was in my post. You have skipped out. OK, it was that exceptions
from declarations is not a good idea. And considering it more deeply,
Eiffel cannot do it either, because specifications are static things. What
you meant is actually "if" in declarations elaboration, which is quite
possible.

>>> 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.
> 
> What is "breach of contract" in your world?

A case for the court.

>> 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.
> 
> Raising of exceptions is an integral part of DbC specs.

And buffer overflow is an integral part of C... I meant static contracts,
statically checked, if that was not clear. It don't need a shortcut for
if-then-raise.

>> 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.
> 
> How would you specify
> 
>    subtype Even is ...; ?

Ada's syntax is:

   subtype <name> is <name> <constraint>;

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