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

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

On Wed, 23 Nov 2011 17:10:41 +0100, Georg Bauhaus wrote:

> On 23.11.11 15:43, Dmitry A. Kazakov wrote:
>> On Wed, 23 Nov 2011 14:59:31 +0100, Georg Bauhaus wrote:
>> 
>>> If it is wrong to assume that a compiler is correct
>> 
>> It is right that the compiler correctly translates your program.
> 
> We do not know whether or not a compiler correctly translates
> a given program unless we show that the translation
> is correct.

It is no matter if we know it or not. The program legality is independent
on that knowledge.

> Is there a compiler out there that is know to work correctly for
> a set of programs?  In this compiler, DbC assertions will
> be documentation only.

Huh, are you going to detect compiler bugs using preconditions? That is the
silliest thing, next to run-time contract checks:

   X := 1;
   if X = 1 then
     -- Wait, that is not enough the compiler might got "=" broken!
     if X/=2 and X/=3 and X/=4 ... X/=Positive'Last then
        -- That must give X=1, but, what if and is broken?
        if not (X=2 or X=3 or X=4 ...
           -- and so on until we notice that X might be actually Y, "if" be
           -- "while" etc

I don't believe Meyer would claim that. Did he?

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