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

[Brian Drummond <brian@shapes.demon.co.uk>]

On Thu, 24 Nov 2011 18:12:30 +0000, Simon Wright wrote:

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

Or,  input above a given peak rate is a violation of the preconditions.

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

Or how much of the system you prove. There are ways to hide the rest from 
the examiner; Barnes has examples involving imported C functions...

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

Yes. Other examples might be a GUI interface to a secure system. You 
would like to prove the input sanitization as well as the secure core, 
but everything outside that is probably a hopeless case...

- Brian