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

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

On 24.11.11 11:52, Dmitry A. Kazakov wrote:

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

Its initial capacity, as outlined in another post.
One may continue with current_number_of_items and such.

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

As a precondition for { Sqrt'Result in Float_Type'Base } the LRM states
{ X in Float_Type'Base and X >= 0.0 }. The precondition of Sqrt in
some language that defines Argument_Error in Float_Type'Base is different.
Not wrong, possibly desirable, but different.


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

Yes, but we do not know before fly-time whether or not there
is going to be enough fuel in the tanks. Flying loops consuming more,
hardware errors caused by people shooting at wings, etc., will not
stop the plane designers to state, using arithmetic expressions,
how much fuel it takes (precondition) to fly from A to B.