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=0.7 required=5.0 tests=BAYES_00,MSGID_RANDY
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,7d1a6bfc6489c17b
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2000-09-08 19:00:11 PST
Path: 
 supernews.google.com!sn-xit-02!sn-east!supernews.com!news-feed.riddles.org.uk!skynet.be!newsfeed.mathworks.com!news.maxwell.syr.edu!nntp2.deja.com!nnrp1.deja.com!not-for-mail
From: Robert Dewar <robert_dewar@my-deja.com>
Newsgroups: comp.lang.ada
Subject: Re: exiting a bloc
Date: Sat, 09 Sep 2000 01:48:33 GMT
Organization: Deja.com - Before you buy.
Message-ID: <8pc4tc$8j1$1@nnrp1.deja.com>
References: <39B15EA8.88DB58AB@netcourrier.com> <8orprn$b46$1@nnrp1.deja.com>
 <39B532CB.73D359F8@ix.netcom.com> <39B5A8B0.56D674C6@telepath.com>
 <39B6114B.2929FA58@amsjv.com> <39B64E94.F081DCAB@telepath.com>
 <8p6bra$g6j$1@nnrp1.deja.com> <PM000370A5FE179FB4@Dogen.ne.mediaone.net>
 <39B72109.89DFAB8C@telepath.com> <PM000370B0EBA888B3@Dogen.ne.mediaone.net>
 <8paf97$ceb$1@trog.dera.gov.uk>
NNTP-Posting-Host: 205.232.38.240
X-Article-Creation-Date: Sat Sep 09 01:48:33 2000 GMT
X-Http-User-Agent: Mozilla/4.61 [en] (OS/2; I)
X-Http-Proxy: 1.0 x72.deja.com:80 (Squid/1.1.22) for client 205.232.38.240
X-MyDeja-Info: XMYDJUIDrobert_dewar
Xref: supernews.google.com comp.lang.ada:553
Date: 2000-09-09T01:48:33+00:00
List-Id: <comp.lang.ada>

In article <8paf97$ceb$1@trog.dera.gov.uk>,
  icaldwell@dera.gov.uk (Ian Caldwell) wrote:

> At least one of the Alsys 'SMART' system, that was produced
for one customer,
> had the requirment to compile the SPARK subset of Ada. I think
that all the
> Alsys 'SMART' system would compile the SPARK subset of Ada.

Right, but talking about the "SPARK subset of Ada" is misleading
sales talk. SPARK is *not* a subset of Ada. The annotations are
a fundamental part of the SPARK language.

Yes, there is a language that is defined as SPARK without any
its annotations, and that is what compilers might well (actually
most certainly *should*) be able to compile, but this is NOT
SPARK. The distinction is important, because if you think of
the SPARK annotations as merely some unimportant documentation,
you are definitely missing the point :-)


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