Re: SPARK and Interfaces.C

[JP Thornley <jpt@diphi.demon.co.uk>]

In article <1116966852.991519.250200@g43g2000cwa.googlegroups.com>, 
ich_bin_elvis@hotmail.com writes
>You were corret about the above my fault so thanks for seeing that. One
>more question and I hope this is the last for my concern for awhile.
>Pragma Import is it okay to use that or is it best to use --#hide
>
>procedure AdaInit;
>   pragma Import (C, AdaInit, "adainit");
>   --  initialize Ada runtime library
>
>   procedure AdaFinal;
>   pragma Import (C, AdaFinal, "adafinal");
>   --  finalize Ada runtime library
>
>adainit and adafinal is not in the adb file since those are imported so
>I get an error. what is done in the real world concerning pragma
>imports?? pragma export is ingored by the examiner but this is not the
>case for ada import
I don't think that there is a universal best answer for this sort of 
question - it all depends on what level of confidence you require for 
the software and how you can get that confidence at minimum cost.

Clearly you are developing a system with some non-SPARK components, and 
so you need to think about how you are going to get the same level of 
confidence in that software as you are getting with the SPARK 
components. You need to identify the SPARK boundary - i.e. what parts of 
the system will be SPARK, and analysable by the tools and what parts 
will be non-SPARK and so require analysis by other means.

You should define the SPARK boundary so that you get the maximum 
confidence in the complete system for the effort that you have available 
(which isn't always achieved by getting as much as possible into SPARK.)

So the answer is to look at the options and pick the one that suits your 
situation.

Cheers,

Phil
-- 
JP Thornley