Re: GNAT packages in Linux distributions

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

On 12.05.10 20:33, Dmitry A. Kazakov wrote:

>> Being better is precisely the point (of DbC).
>> DbC talks about proof obligations, not about provability.
> 
> Who is obliged to whom in what?

By being a programmer subscribing to the principles of DbC,
you are obliged to show that the components of your system
obey the components' contracts.  The compiler and run-time
try to help you achieving this goal.


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

Which set of "specifications" has only static things in it?
Why exclude conditionals whose results cannot reasonably
be computed by the compiler but

(a) can be computed for every single case occuring in the
executing program

(b) can guide the author of a client of a DbC component?


For example, assume that Is_Prime(N) is a precondition of sub P.
Furthermore, TIME(Is_Prime(N)) >> PERMISSIBLE_TIME.
Then, still, PRE: Is_Prime (N) expresses an obligation,
part of a contract:  Don't call P unless N is prime,
no matter whether or not assertion checking is in effect.

(A DbC principle is that assertions are *not* a replacement
for checking input (at the client side).)




>> What is "breach of contract" in your world?
> 
> A case for the court.

What's the court (speaking of programs)?


>>> 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 wasn't clear to me that you wanted a mathematically closed structure
to be the only legitimate substance of "contract".
I'm a programmer.  If I "design" anything, it is a program whose
parts need to interact in a way that meets some almost entirely
non-mathematical specification.  I try to add some formality
to the whole thing.  This helps. I wish I had static type checking
for a start!



>> How would you specify
>>
>>    subtype Even is ...; ?
> 
> Ada's syntax is:
> 
>    subtype <name> is <name> <constraint>;


What will static <name> and static <constraint> be for subtype Even?