Re: exiting a bloc

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

In article <8papum$kaf$1@nnrp1.deja.com>,
  r_c_chapman@my-deja.com wrote:
> And for desserts - the shocking realisation that Robert got
> something wrong on c.l.a - Praxis certainly don't
> make a compiler for SPARK - we make a static analysis
> tool called the Examiner.
>
> SPARK is compiled with any standard Ada compiler,
> including those hosted on and/or targetting SPARC(tm)
> and or using [C-]SMART as a runtime  (or RAVEN, VADSsc,
> ApexMARK, GNORT, Integrity etc. etc.)!


Actually I sort of think of Examiner as a compiler for SPARK
in the sense that a critical part of any compiler is semantic
verification that the program is legal, and that is what
the examiner does. Yes, there is also the little detail of
generating code once this semantic checking is complete, but
any old Ada compiler can do that :-)

So really a SPARK compiler must do both annotation checking
and the normal code generation of a compiler, so the way you
get a compiler for SPARK today is to put the Examiner together
with a compiler (such as GNAT :-).

So Rod is quite right, I should not have said that Praxis has
a compiler for SPARK, I should have said that they make the
most critical part of the SPARK compiler!

Actually a full blown integrated compiler for SPARK might well
be able to take advantage of the annotations to improve code
quality, eliminate checks etc, but so far no one has produced
such a beast.


Sent via Deja.com http://www.deja.com/
Before you buy.