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

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

On 23.11.11 15:43, Dmitry A. Kazakov wrote:
> On Wed, 23 Nov 2011 14:59:31 +0100, Georg Bauhaus wrote:
> 
>> On 23.11.11 14:14, Dmitry A. Kazakov wrote:
>>> On Wed, 23 Nov 2011 12:25:56 +0100, Georg Bauhaus wrote:
>>>
>>>> On 23.11.11 12:13, Dmitry A. Kazakov wrote:
>>>>> On Wed, 23 Nov 2011 12:03:34 +0100, Georg Bauhaus wrote:
>>>>>
>>>>>> On 23.11.11 10:56, Dmitry A. Kazakov wrote:
>>>>>>
>>>>>>> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a part
>>>>>>> of the implementation?
>>>>>>
>>>>>> I don't agree. pre/post should specify what the implementation is
>>>>>> supposed to do.
>>>>>
>>>>> In that case they cannot be executable.
>>>>
>>>>  From the point of view of CS trivia, they cannot be executable.
>>>> But this point of view is not applicable,
>>>
>>> I don't see why doing something wrong should make it more applicable. Maybe
>>> because the criteria of applicability are distorted as well?

Because it leads to self documenting source text that
uses this wrong formalism, assertions.


>> 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. If we do, we know that the given run of the compiler
on the given program seems to have worked as intended. (ACATS)
The only check in a compiler without internal checks is a translation
that is checked by humans.  A compiler that performs internal checks
while it is running may fail and produce a notice of failure.
Perhaps it should continue instead and produce a program that
shifts a rocket?

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.

> Are you
> suggesting to break the compiler because it might be already broken?

No.