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

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

On Thu, 24 Nov 2011 15:31:27 +0100, Georg Bauhaus wrote:

> On 24.11.11 14:14, Dmitry A. Kazakov wrote:
> 
>> There is no such thing as assumption, there are only conditions for
>> whatever outcome of which, the program's behavior must be defined.
> 
> When I state a condition and have no proof that the condition
> is correct WRT such-and-such, then my statement is based on
> assumptions.

No, "if A then B" is not based on an assumption of A. B is (in this
context).

> BTW, assuming looks like a normal mathematical gesture to me:
> "Assuming that P(x, y) is true, we show that Q(x, y, z) is true."
> Why do mathematicians do this if their work hinges on statically
> unproven P(x, y)?

Because the mathematician usually stops at P|=Q. In programming you are
interested in both P|=... and ^P|=..., so long P is not proven.

>>> Like when showing that for a stack object, the sequence
>>> (not Is_Full, Push, Pop) is a safe sequence,
>> 
>> It is not safe:
> 
> I didn't say that it is safe. I said it is (a) safe sequence, ceteris
> paribus (listing these) and (b) safe sequence because, to quote you,
> "The contract might imply behavior (safety of this sequence
> under certain conditions), when provable."  The sequence of operations
>   (not Is_Full, Push, Pop)
> is provably o.K. by the contract shown because of a 1:1 correspondence
> of the type's invariant (ensuring capacity and not Is_Full),
> the postconditions and preconditions at each step. Therefore,
> checks will be redundant.

OK
 
>> 2. immutable stack has one Is_Full.
> 
> If by immutable you mean a constant view, what's the point?

That the proposition does not hold for all instances of stack.

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