From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,ea5071f634c2ea8b
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.15.105 with SMTP id w9mr8826882pbc.7.1322158351628;
        Thu, 24 Nov 2011 10:12:31 -0800 (PST)
Path: 
 lh20ni13592pbb.0!nntp.google.com!news1.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.musoftware.de!wum.musoftware.de!news.swapon.de!eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug.
Date: Thu, 24 Nov 2011 18:12:30 +0000
Organization: A noiseless patient Spider
Message-ID: <m24nxt8k4x.fsf@pushface.org>
References: 
 <7bf9bc32-850a-40c6-9ae2-5254fe220533@f29g2000yqa.googlegroups.com>
	<wcc1ut14o97.fsf@shell01.TheWorld.com>
	<128rdz2581345$.c4td19l7qp9z$.dlg@40tude.net>
	<jaecvt$4tp$1@dont-email.me>
	<16ipwvpdavifr$.17bxf7if7f6kh$.dlg@40tude.net>
	<4ecb78b1$0$6643$9b4e6d93@newsspool2.arcor-online.net>
	<1iofgbqznsviu$.phvidtvxlyj4$.dlg@40tude.net>
	<4ecbb96e$0$6581$9b4e6d93@newsspool3.arcor-online.net>
	<vagow98uvk3n$.198v2ms719j4e$.dlg@40tude.net>
	<4ecbdfdb$0$6629$9b4e6d93@newsspool2.arcor-online.net>
	<12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net>
	<jah2np$7fp$1@munin.nbi.dk>
	<1ecuhb030iugz.4q1hfjx371xa.dlg@40tude.net>
	<4ecc393d$0$7625$9b4e6d93@newsspool1.arcor-online.net>
	<124aq618dmove.884jj64mzm6w$.dlg@40tude.net>
	<m2mxbn89qz.fsf@pushface.org>
	<1jxx617mf2cqf$.1j076axdq83mr$.dlg@40tude.net>
	<m2d3ci98l4.fsf@pushface.org>
	<1cjufyo57vlpg$.11kf45cs5vnb7.dlg@40tude.net>
	<m28vn67xke.fsf@pushface.org> <jal90n$c4u$1@dont-email.me>
Mime-Version: 1.0
Injection-Info: mx04.eternal-september.org;
 posting-host="dFCm8HWntFqmDIilBLqEJQ";
	logging-data="2380"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18ERa6i/RnW1yBy4Kh+ZRKvsTeej5BDWv0="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.3 (darwin)
Cancel-Lock: sha1:VKKgB0AqnTM4fRorZnUnedPfXJc=
	sha1:pS+YI45lcaqEue7rWh9LgoNk3DQ=
Xref: news1.google.com comp.lang.ada:19121
Content-Type: text/plain; charset=us-ascii
Date: 2011-11-24T18:12:30+00:00
List-Id: <comp.lang.ada>

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!