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, MSGID_RANDY 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: Peter Amey Subject: Re: Suitability for small Windows projects Date: 2000/10/23 Message-ID: <8t1ppg$70o$1@nnrp1.deja.com>#1/1 X-Deja-AN: 684864680 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> X-Http-Proxy: 1.0 PROXY, 1.0 x73.deja.com:80 (Squid/1.1.22) for client 193.114.91.187 Organization: Deja.com - Before you buy. X-Article-Creation-Date: Mon Oct 23 16:42:27 2000 GMT X-MyDeja-Info: XMYDJUIDpeteramey Newsgroups: comp.lang.ada X-Http-User-Agent: Mozilla/4.73 [en] (WinNT; U) Date: 2000-10-23T00:00:00+00:00 List-Id: In article , Robert A Duff wrote: > 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! I really hope we can and with judicious use of attributes we may be able to. The idea of formally proven, exception-free, re-usable components has a certain attraction. It's just a bit too early to say. > > > 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?) We will almost certainly adopt the view of prohibiting instantiation with Boolean since all the alternatives would unduly restrict the use generics could be put to. Booleans were origially not ordered because the underlying language we use for proof (FDL - Functional Description Language) does not have them it was possible to construct rather esoteric invalid proofs by taking advantage of that fact. There has been a useful payoff in our proof of exception freedom work: Boolean expressions in SPARK cannot raise constraint errors. For example you can't take 'Succ of True or other sillies. The limitation is not too restrictive in practice and we sugar the pill by allowing Boolean'first and 'last but just defining them to be synonyms of False and True. So the only things really missing are <, >, Succ and Pred. [snip] > > 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)? I don't think we _know_ it can't be done but it certainly is "a big chunk of work"! The usual SPARK tradition is to try and get something useful into the language and do the gold-plating later; I would be very pleased to do this with a limited form of generics and worry about subprogram parameters later. Thanks for the ideas and interest. Peter Sent via Deja.com http://www.deja.com/ Before you buy.