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

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

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. Let's be honest.

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

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

> 2. immutable stack has one Is_Full.

If by immutable you mean a constant view, what's the point?
If by immutable you mean a discriminant won't change,
Is_Full may still not be constant function. I guess I don't understand.


> It is also pointless to use undecidable propositions for static proofs
> (which is basically the idea behind dynamic checks). Garbage in, garbage
> out.

Yes. If I knew SPARK better, I might say something about
proof functions, but I don't.