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

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

On Thu, 24 Nov 2011 02:36:47 +0100, Georg Bauhaus wrote:

> On 23.11.11 20:48, Dmitry A. Kazakov wrote:
> 
>>>>> Subprograms of unknown effect,
>>>>
>>>> You confuse interface and implementation.
>>>
>>> I call a subprogram because it has an effect. Is this unusual?
>>> In order to choose the right subprogram, I need to know its
>>> effect.
>>
>> That is exactly why contracts cannot be dynamic. Dynamic means statically
>> undecidable. How are you going to know anything about the subprogram, if
>> that is unknown until run-time?
> 
> The typical example is a stack and its contract referring to
> values available at runtime: from the contract, I learn that a stack
> is initially empty and has a certain capacity.

What is dynamic there?

> Similarly, for Sqrt, Ada throws Argument_Error if the caller
> fails to establish the implicit precondition of Sqrt:

It is not a precondition, sqrt (-1.0) is *defined* as Argument_Error
propagation. I.e. the postcondition includes Argument_Error. The
precondition is "X in Float."

> Is Sqrt'Result statically determinable?

The semantics of sqrt can be formally defined as it happens in math. For an
arithmetic based on bounded rational numbers with rounding errors (e.g.
Float) it is also possible, but nobody would care.

>>>>>>> There is no right or wrong in most programs.
>>>>>>
>>>>>> You cannot build safe software on false premises.
>>>>>
>>>>> Almost all programs have a number of things that can go wrong,
>>>>
>>>> Program code cannot GO wrong, it IS either wrong or not, here and now.
>>>
>>> No, we don't know whether an executable program is right or wrong,
>>> for almost all programs.
>>
>> It is not about anybody's knowledge. A program is correct or not
>> independently on whether you or anybody else knows that.
> 
> "Is correct or not correct" sounds like a tautology and says just
> as much.

It says that correctness is unconditional to our ability to decide it. [It
is conditional to the specifications only] 

A plane without fuel would crash regardless your ability to determine the
level kerosene in its tanks.

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