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 X-Google-Thread: 103376,7d1a6bfc6489c17b X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2000-09-13 01:34:03 PST Message-ID: <39BF3C11.CA3A9347@amsjv.com> Date: Wed, 13 Sep 2000 09:34:25 +0100 From: Philip Anderson Organization: Alenia Marconi Systems ISD X-Mailer: Mozilla 4.7 [en] (WinNT; I) X-Accept-Language: en MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: exiting a bloc 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> Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit NNTP-Posting-Host: 141.196.71.137 X-Trace: 13 Sep 2000 09:30:00 GMT, 141.196.71.137 Path: supernews.google.com!sn-xit-02!sn-xit-03!supernews.com!europa.netcrusader.net!128.230.129.106!news.maxwell.syr.edu!btnet-peer!btnet!newreader.ukcore.bt.net!pull.gecm.com!141.196.71.137 Xref: supernews.google.com comp.lang.ada:620 Date: 2000-09-13T09:34:25+01:00 List-Id: 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. -- hwyl/cheers, Philip Anderson Alenia Marconi Systems Cwmbr�n, Cymru/Wales