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.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,be3749d096f8436b X-Google-Attributes: gid103376,public From: Robert A Duff Subject: Re: Suitability for small Windows projects Date: 2000/10/23 Message-ID: #1/1 X-Deja-AN: 684842391 Sender: bobduff@world.std.com (Robert A Duff) References: <8qr809$cjj@newshost.fujitsu.com.au> <8qrs0i$kq2@newshost.fujitsu.com.au> <8qs469$pf1@news.kvaerner.com> <39D1C1F3.893B61A6@maths.unine.ch> <8qtsek$j7c$2@news-hrz.uni-duisburg.de> <8qvj52$1lm$1@nnrp1.deja.com> <8smc96$hs7$1@nnrp1.deja.com> <8ss9fb$6m7$1@nnrp1.deja.com> <8t1d7l$sd2$1@nnrp1.deja.com> Organization: The World Public Access UNIX, Brookline, MA Newsgroups: comp.lang.ada Date: 2000-10-23T00:00:00+00:00 List-Id: Peter Amey writes: >... (We may still have to prove freedom from exceptions on an > instantiation-by-instantiation basis but that is another story). I don't see why you can't do it in an assume-the-worst way. And it seems desirable to make the proof totally independent of the instantiation. Otherwise, your proofs are violating the contract model! > As an example of the kind of difficulty we have to take into > account (not an 83 vs 95 issue in this case), consider a discrete type > parameter. This would allow the ordering operators to be used as well > as things like 'Pred/'Succ. Boolean would be a valid match for the > parameter; however, SPARK does not consider Booleans to be ordered so > the body would be illegal in this case. No, if you don't want Booleans to be ordered, then SPARK should disallow instantiating with Boolean. (By the way, *why* are Booleans not ordered in SPARK?) > Our best guess is that will allow parameterisation by type (e.g. stack > of widgets, stack of thingies); parameterisation by some constant (e.g. > stack capable of holding N things); and parameterisation by some literal > value (e.g. port-inboard engine controller, starboard-outboard engine > controller). Subprogram parameters and generic packages seem rather > unlikely at present. What's the difficulty with subp params? They of course have to have pre- and postconditions, and you would need to prove that the precondition of the formal implies the precondition of the actual and so forth. Also globals annotations? Are there any specific problems (other than the fact that it's a big chunk of work)? - Bob