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: <8t1d7l$sd2$1@nnrp1.deja.com>#1/1 X-Deja-AN: 684787747 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> X-Http-Proxy: 1.0 PROXY, 1.0 x64.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 13:08:08 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 <8ss9fb$6m7$1@nnrp1.deja.com>, Robert Dewar wrote: > In article <8smc96$hs7$1@nnrp1.deja.com>, > r_c_chapman@my-deja.com wrote: > > We're thinking about it, but it's a fair way off yet. Some > history: > > generics were broken in Ada83 to a point where they simply > couldn't > > be seriously considered for SPARK83. In Ada95, things are > better, > > so there's some possiblility of a limited form of generic > units in > > SPARK95 - the main restriction will be, of course, on the form > > of generic formal parameters allowed. > > I don't buy the above for a moment, there is no HUGE difference > between Ada 83 and Ada 95 here, given that SPARK would only > allow a limited form of generics in either environment. > I hate disagreeing with Robert because it is such a reliable way of making yourself look stupid; however, I have to risk it in this case. Generics were not included in SPARK 83 for three reasons: 1. We wanted to write a formal definition of SPARK and were not at all sure we could do it for generics. I believe this has been a tricky area for some of the attempts to produce formal definitions of Ada. 2. Complexity: we wanted SPARK to be a simple language with simple semantics. It was not at all clear that we could defined a subset of SPARK 83 generics that would be useful, simple and maintain SPARK's properties of compiler-independence, elaboration-order independence etc. 3. As Rod alluded to in his reply, the SPARK 83 generic contract model is indeed "broken". This is freely acknowledged in the Ada 95 Rationale in Section II.11 which actually uses the word "broken"! We are looking at generics for SPARK 95 with the objective of being able to annotate generics such that their annotations will be valid for any instantiation. In principle this could give use "re-usable proof". The changes to the generic parameter model of SPARK 95 are essential for this. (We may still have to prove freedom from exceptions on an instantiation-by-instantiation basis but that is another story). 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. 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. regards Peter Sent via Deja.com http://www.deja.com/ Before you buy.