Re: Ada used in General Aviation (GA) applications?

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

Marin David Condic wrote:
> The "Compile Ada to C then compile C to the target..." approach has been 
> enormously popular and successful, hasn't it? :-)

Yes, considering we only came up with the SPARK -> C idea last year it 
has been rather popular :-)

> Nobody wants to use two compilers, nobody wants to cobble the whole mess 
> together and nobody wants to fight all the rest of the development tools 
> that will be targeted to C. The whole argument amounts to "Go out and 
> spend lots of extra money, take lots of extra time and go through lots 
> of extra pain in order to have the *privilege* of programming your 
> little board in Ada - all for a job that might only involve a couple of 
> guys for a few months." It has not sold well and I doubt it ever will. 
> Ada is either right there on the shelf with an embedded development kit 
> or the embedded guys go elsewhere.

There is some truth in what you say, the process has to be convenient. 
I think this hinders use of the approach for Ada in general.  The use of 
SPARK changes the gearing somewhat:

1.  You are achieving more than "the privilege of programming your 
little board in Ada", you are gaining the ability to do very high levels 
of validation much earlier in the development process.  Before you even 
get to C you can have eliminated use of unset variables, proved freedom 
from all run-time errors, shown that values remain in 
design-domain-defined ranges (regardless of what C predefined type they 
end up being implemented as), demonstrated separation of critical and 
non-critical information flows and even proved that certain important 
properties of the code hold.

2.  The translation process can be completely transparent.  As far as we 
are concerned on one project, we have what amounts to a SPARK to target 
compiler.  We don't need to process the C manually at all.

3.  If you are constrained to deliver something like MISRA-C then it is 
orders of magnitude easier to arrange for the translator to represent 
the exact SPARK design in something which is unequivocally MISRA-C than 
to demonstrate retrospectively that hand-crafted C conforms to the 
subset rules.

4.  For very critical applications, the C provides an intermediate 
representation between the SPARK and the object code and this makes 
object code verification much easier than it otherwise would be.  For 
example, array assignments at the Ada level are "unwrapped" at the C 
level.  This intermediate representation allows one very hard step: 
comparing Ada to machine code to be replaced by two much easier ones: 
Ada to (simple) C and C to machine code.

5.  You don't need, and therefore don't have to validate, a run-time 
library.

So far from having to "spend lots of extra money, take lots of extra 
time and go through lots of extra pain" we find the combination allows 
us to produce higher quality at lower cost than writing directly in C.

regards


Peter