From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,3a4656a5edc0dab4 X-Google-Attributes: gid103376,public Path: controlnews3.google.com!news2.google.com!fu-berlin.de!uni-berlin.de!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: Ada used in General Aviation (GA) applications? Date: Thu, 13 May 2004 08:43:17 +0100 Message-ID: <2ggn4gF2no0lU1@uni-berlin.de> References: <409F69CB.8020604@noplace.com> <2geb04F1pte3U1@uni-berlin.de> <40A21D65.7050806@noplace.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: http://news.individual.net/abuse.html X-Trace: news.uni-berlin.de 7D9tEuBPn7VDUSvj8rLROwvdKExoMV3eId0bHOQH1x2/FnFlE= User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.4) Gecko/20030624 Netscape/7.1 (ax) X-Accept-Language: en-us, en In-Reply-To: <40A21D65.7050806@noplace.com> Xref: controlnews3.google.com comp.lang.ada:523 Date: 2004-05-13T08:43:17+01:00 List-Id: 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