Re: GNAT packages in Linux distributions

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

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.

> 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 ... .


>> 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.

If you say

 Precondition: Has-Such-And-Such;

then this is effectively

 raise when not Has-Such-And-Such;

Except that smart tools do not need to understand the full program
including its bodies in order to infer a precondition.


>> 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?

Anything that is not yielding a full proof of everything is
a debugging tool.
So what?
Should we therefore bend the normal, worldly definition of
"contract" to mean something that can never be had?


> 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.

Purity:

  postcondition: interesting_1 = interesting_1'old
     and interesting_2 = interesting_2'old
     and ...;

Stack usage:

   precondition: avail = max_avail - 140;

> 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 ...; ?