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: r_c_chapman@my-deja.com
Subject: Re: Suitability for small Windows projects
Date: 2000/10/19
Message-ID: <8smc96$hs7$1@nnrp1.deja.com>#1/1
X-Deja-AN: 683224783
References: <8qr809$cjj@newshost.fujitsu.com.au>
 <slrn8t2cih.8d9.haering@sunhalle3.informatik.tu-muenchen.de>
 <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>
 <Pine.BSF.4.21.0009280825480.29105-100000@shell5.ba.best.com>
X-Http-Proxy: 1.0 PROXY,
 1.0 x62.deja.com:80 (Squid/1.1.22) for client 193.114.91.187
Organization: Deja.com - Before you buy.
X-Article-Creation-Date: Thu Oct 19 08:44:23 2000 GMT
X-MyDeja-Info: XMYDJUIDr_c_chapman
Newsgroups: comp.lang.ada
X-Http-User-Agent: Mozilla/4.73 [en] (WinNT; U)
Date: 2000-10-19T00:00:00+00:00
List-Id: <comp.lang.ada>

In article
<Pine.BSF.4.21.0009280825480.29105-100000@shell5.ba.best.com>,
  Brian Rogoff <bpr@shell5.ba.best.com> wrote:

> And, since it is more relevant to Ada, what of generics in SPARK? I
> remember asking about this a long time ago and someone from Praxis
said
> a future version might support some form of generics.

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.

A particular issue would be the validity of the Examiner's static
analysis: we'd like the analysis results for a generic body
to be valid for all possible instantiations of that body.  This is
probably achievable for the static semantic rules (including flow
analysis), but looks far more difficult for the proof stuff - exception
freedom proofs critically depend on statically knowing attributes
such as 'First and 'Last of types, so we might have to do VC
generation on a per-instantiation basis.  This is hard, since
it imples implementing at least a simple form of expander
phase in the Examiner - something we currently don't have!

As always, we'll listen to users' requests, but this is not
currently a high-priority.
 - Rod Chapman
   SPARK Team
   Praxis Critical Systems


Sent via Deja.com http://www.deja.com/
Before you buy.