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

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

On Thu, 24 Nov 2011 08:07:45 +0000, Simon Wright wrote:

> To take Georg's example of the stack, I don't see how you're going to
> express the fact that its capacity is bounded other than by comments
> about constraint errors or by preconditions.

The point is that when this behavior can be expressed then that expression
is static, per definition of the word "expressed." When it cannot be
expressed then it is not.

A dynamic precondition does not express anything, because it is unknown
until run-time. If it is known, then it is not dynamic.

> I seem to be tempted into speculations about SPARK at this point. Stacks
> seem to be a rather dangerous construct from the point of view of
> proving correctness, logic not being very good at counting.

SPARK does it right, Eiffel and now Ada do it wrong.

My plea is not to full ourselves. If correctness cannot be proved
statically, then the requirement expressed by the precondition must be
considered as not satisfied. That precondition must be replaced by "true",
and the corresponding exception (Stack_Full) added to the postcondition.
The clients must respect this new contract and handle Stack_Full.

I would like Ada integrated rather with SPARK than with Eiffel, allowing
the programmer to choose between static correctness and, when that does not
work or seem to be too expensive, contracts extended with exceptions.

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