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

[Simon Wright <simon@pushface.org>]

Brian Drummond <brian@shapes.demon.co.uk> writes:

> Indeed. But if you also prohibit recursion, maximum stack use is
> provable.

Maximum use of a bounded buffer faced with a peaky input is probably
less provable. At least you have more potential solutions there; throw
away the earliest, throw away the latest, throw away the least
important.

> But the state of the art seems to be that for contracts to be
> statically determinable, you must restrict how you program, compared
> to full Ada.

And maybe the sort of system you try to prove?

The provably-correct part of a system will probably not be the whole of
it, not of course that that releases us from the obligation to prove as
much as possible. Even Tokeneer would have needed mitigations against
villains with chainsaws.

> In this world, I come down on the side of: dynamically determinable
> contracts may not be perfect, but they are a lot better than
> nothing. I would use them and try to create tests to catch them out.

A real-world approach!