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-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,b761e94375940f9f
X-Google-Attributes: gid103376,public
X-Google-Thread: 108717,b761e94375940f9f
X-Google-Attributes: gid108717,public
X-Google-Thread: 115aec,b761e94375940f9f
X-Google-Attributes: gid115aec,public
X-Google-Thread: f43e6,b761e94375940f9f
X-Google-Attributes: gidf43e6,public
X-Google-ArrivalTime: 2002-07-13 13:15:19 PST
Path: archiver1.google.com!postnews1.google.com!not-for-mail
From: rod@praxis-cs.co.uk (Rod Chapman)
Newsgroups: comp.lang.ada,comp.realtime,comp.programming,comp.software-eng
Subject: Re: ANNOUNCE: SPARK toolset 6.1 now available
Date: 13 Jul 2002 13:15:19 -0700
Organization: http://groups.google.com/
Message-ID: <ba18d5cb.0207131215.4f0d7@posting.google.com>
References: <ba18d5cb.0207102357.27f22745@posting.google.com>
 <4519e058.0207110604.62691233@posting.google.com>
 <ba18d5cb.0207120052.10747fd6@posting.google.com>
 <uiuecbr38qbc34@corp.supernews.com> <x7vd6tr4ulf.fsf@pushface.org>
 <wccwurzzpb7.fsf@shell01.TheWorld.com>
NNTP-Posting-Host: 213.152.53.239
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: posting.google.com 1026591319 17095 127.0.0.1 (13 Jul 2002 20:15:19
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: 13 Jul 2002 20:15:19 GMT
Xref: archiver1.google.com comp.lang.ada:27064 comp.realtime:5844
 comp.programming:35117 comp.software-eng:12109
Date: 2002-07-13T20:15:19+00:00
List-Id: <comp.lang.ada>

In answer to several points:

1) No - we don't currently allow 'Class anywhere, which means heterogeneous
lists are not supported directly in SPARK, although these may
be achieved by suitable hiding and abstraction.

2) SPARK does not currently include access type of any kind, since these
create some very difficult problems with the analysis of pointer effects
and aliasing.  If we can work out the analysis, then including some
support for general access types in future may in within scope.

3) Whether the restrictions implied by points 1) and 2) constitute
a "useful subset" of tagged types is really a matter of taste and outlook.
I guess time will tell if our users find the existing subset useful
for writing real programs of not...

Finally, in answer to Bob's point:

> If you have the entire program source code (which you should in a
> safety-critical context), then I don't see why a dispatching call is any
> more "uncertain" than a case statement.

But waiting until you have the "entire program" is _way_ too late!  One of
the major design goals of SPARK is to enable _constructive_ static
analysis of incomplete programs - hence the need for annotations
to strengthen the contracts in package specifications, for instance.

 - Rod Chapman, SPARK Team, Praxis Critical Systems.