Re: exiting a bloc

[Robert Dewar <robert_dewar@my-deja.com>]

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.