Re: exiting a bloc

[Peter Amey <pna@praxis-cs.co.uk>]

In article <39BF3C11.CA3A9347@amsjv.com>,
  Philip Anderson <phil.anderson@amsjv.com> 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.