Re: exiting a bloc

[Philip Anderson <phil.anderson@amsjv.com>]

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