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

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

On Tue, 22 Nov 2011 18:46:02 +0100, Georg Bauhaus wrote:

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

Any discussion should be based on the meaning of words.

Discussions about words are uninteresting to me.

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

I see no word "debugging" there.

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

I suppose drinking coffee does that as well. CDD [caffeine driven design]
(TM). As for randomly raised exceptions from dynamic checks, I doubt that
leads to better products. I my experience at least 40% of my debugging
efforts in Ada 95 was spent on catching accessibility checks faults. Ada
2005 improved that greatly. To me this is a vivid example why dynamic
checks are evil.

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

If the program has a bug its execution is erroneous. Is it what you want to
say? So?

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

Which then? You have to specify the failures you are going to notice. Once
you do qualify them, you would easily be able to avoid them. Note that all
the buzz is about noticing something unanticipated. That is impossible,
period. Anticipated failures are not bugs, they are states.

>> The software which behavior is unknown shall never be executed.
> 
> But this is impossible, in general!

I see the point, since it is impossible do right, you are going to do it
wrong. I am not arguing for or against your or Meyer's motivations. I only
state that it is wrong. 

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