Re: Generic-Package Elaboration Question / Possible GNAT Bug.

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

On 22.11.11 17:23, Dmitry A. Kazakov wrote:

>> Not sure, are you speaking about DbC (TM)?
> 
> I don't care about trade marks and definitions given by reference
> manuals...

Frankly, doing so in some way will help discussing things.

DbC is ...
>> (b) A debugging ("design", "specification", bla-bla) aid leading
>>     towards formally proven components where such proofs are possible.
> 
> I cannot decipher this, sorry.

Meyer: "Programming is a human activity".
Programmers are led towards a solution during the process of programming.
Depending on the characteristics of the process, then,
programmers will produce different results.
DbC (TM), as a characteristic of a process, leads to products
that lend themselves to proving them correct more than others,
provided this is possible.


>> "An exception is the element's inability to fulfil its contract, for any
>> reason: a hardware failure has occurred, a called routine has failed, a
>> software bug makes it impossible to satisfy the contract."
> 
> An exception is a program state. It is not an inability. The behavior in an
> exceptional state is contracted, at least in Ada it is.

OK, erroneous execution. A program's behavior according to the contract.
Yes. But lame.


>> Without those dynamic checks, we wouldn't ever notice a failure?
> 
> How would you notice a failure to notice?

Really does not matter. There is no need to require forall-qualification
of every aspect of DbC(TM) when it is not meant to be in a program
if and only if the program (including hardware) is proven to be
100% such-and-such.  Impractical.

> The software which behavior is unknown shall never be executed.

But this is impossible, in general!