Re: Ada to C++ translator?

[Nick Williams <nickw@acm.org>]

Marin David Condic wrote:


>> There's a difference between a compiler which doesn't support the full
>> language and a project choosing not to use the full language!

> And your point would be? :-) Seriously, I understand there is a distinction,
> but I don't know that it makes any difference. SPARK is a chosen subset of
> Ada and I'd presume that if one bought the SPARK compiler that it would
> compile only the SPARK subset. (Or at least someone might choose to
> implement a compiler for SPARK that way.)

You'd have difficulty buying the SPARK compiler; as there isn't one :-)

From the Ada perspective, SPARK is indeed a subset; since whatever is a valid 
SPARK program is also a valid Ada program, but the converse does not hold.

However, just because an Ada program uses the subset of the Ada language which
is valid in SPARK will (most likely) not make that program valid in SPARK: the
SPARK language has a considerable variety of non-compilable statements (which
look to an Ada compiler like comments) which are not optional when constructing
SPARK programs. It also has restrictions on the use of language features which
can make it harder to prove properties of your program.

> (SPARK doesn't call itself "Ada" and isn't validated, right?) 

Well, the 'A' in SPARK does stand for Ada ... and the only validation is 
a relatively detailed and complete formal semantics of the language :-)

Cheers,

Nick.