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-13 04:10:06 PST Path: supernews.google.com!sn-xit-02!sn-xit-03!supernews.com!xfer13.netnews.com!netnews.com!news.maxwell.syr.edu!nntp2.deja.com!nnrp1.deja.com!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: exiting a bloc Date: Wed, 13 Sep 2000 11:02:55 GMT Organization: Deja.com - Before you buy. Message-ID: <8pnmsn$7cn$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> <39B72109.89DFAB8C@telepath.com> <8paf97$ceb$1@trog.dera.gov.uk> <8pc4tc$8j1$1@nnrp1.deja.com> <8pl3qa$ivi$1@trog.dera.gov.uk> <8pm2qi$bjl$1@nnrp1.deja.com> <39BF3C11.CA3A9347@amsjv.com> NNTP-Posting-Host: 193.114.91.187 X-Article-Creation-Date: Wed Sep 13 11:02:55 2000 GMT X-Http-User-Agent: Mozilla/4.73 [en] (WinNT; U) X-Http-Proxy: 1.0 PROXY, 1.0 x58.deja.com:80 (Squid/1.1.22) for client 193.114.91.187 X-MyDeja-Info: XMYDJUIDpeteramey Xref: supernews.google.com comp.lang.ada:623 Date: 2000-09-13T11:02:55+00:00 List-Id: In article <39BF3C11.CA3A9347@amsjv.com>, Philip Anderson wrote: > Robert Dewar wrote: > > > > In article <8pl3qa$ivi$1@trog.dera.gov.uk>, > > icaldwell@dera.gov.uk (Ian Caldwell) wrote: > > > When I used "the SPARK subset of Ada" I meant SPARK without > > any of its > > > annotations. I know that not the full SPARK language. Maybe I > > should have used > > > the Ada subset of SPARK (meaning the part of SPARK that is > > Ada). > > > > It would be convenient (and perhaps avoid confusion) to have > > a clear name for that subset :-) > > Praxis refer to the overlap between SPARK and Ada as "the common > kernel"; the SPARK core is then this common kernel + the core > annotations (there are also optional proof annotations). The SPARK Ada > kernel is probably the least ambiguous term. > > For those who don't know, the SPARK annotations take the form of Ada > comments with a defined syntax, all beginning --# (or --$ in our case), > and so a SPARK program is legal Ada and can be compiled by any Ada > compiler; the SPARK Examiner is an additional tool which does not > compile but verifies the SPARK code (the Ada kernel + annotations). In > addition, something like Rational's Apex Ada Analyser can be set up to > analyse an Ada program and flag non-SPARK Ada, but that does nothing > with annotations of course. > It is important to realise, however, that without the mandatory annotations it is extremely hard (impossible without a 'whole program' analysis) to say whether a piece of code is written in SPARK or not. It is only the presence of annotations that makes, for example, aliasing and function side effects (both prohibited in SPARK) detectable in reasonable computation times or in incomplete programs. The elimination of errors at the coding stage is one of the factors that makes SPARK use so cost effective; certainly it is better than waiting until the code is finished and then trying to find errors retrospectively. Analysers (other than the SPARK Examiner of course) which claim to check for SPARK compliance only do very crude checking for major prohibited constructs such as tasking or the use of "new". Peter Sent via Deja.com http://www.deja.com/ Before you buy.