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

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

On Thu, 24 Nov 2011 11:49:30 +0100, Georg Bauhaus wrote:

> On 24.11.11 10:27, Dmitry A. Kazakov wrote:

>> If correctness cannot be proved
>> statically, then the requirement expressed by the precondition must be
>> considered as not satisfied.
> 
> We may state our assumptions and have them checked,

There is no such thing as assumption, there are only conditions for
whatever outcome of which, the program's behavior must be defined.

> Like when showing that for a stack object, the sequence
> (not Is_Full, Push, Pop) is a safe sequence,

It is not safe:

1. finalization and initialization may fail in Ada. The contracts of
element and index types propagate into the contracts of the container.

2. immutable stack has one Is_Full.

And it is the behavior, not the contract. The contract might imply behavior
(safety of this sequence under certain conditions), when provable. If not
provable, adding dynamic checks in all possible places trying Push and Pop
would be pointless. Not proven means: expect any outcome (any = anything
not excluded by a proof).

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

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