Re: Safety Critical Systems and Ada 95

[jpt@diphi.demon.co.uk (JP Thornley)]

In article: <357EB552.5CF3EB9@swl.msd.ray.com>  "John J Cupak Jr, CCP" 
<jcj@swl.msd.ray.com> writes:
> 
> I know Ada 95 has a Safety Annex, but has anyone actually used
> it to implement a real (or even example) system?
> 
> Are there any specific reports or papers on the Safety features
> of Ada 95 (other than RM95 or the Rationale)?
> 
> Inquiring minds want to know!
> 

There are (AFAIK) no compilers that implement Annex H (but there are no 
tests for conformance either!).

[But I've just remembered that GNAT claims to implement 100% of the 
language - must see what they do for the Annex H pragmas.]

It's important to realise that pragma Restrictions does not *impose* 
that restriction on the code. ARM 13.12 says "A pragma Restrictions 
expresses the user's intent to abide by certain restrictions." and if 
the user breaks the restriction the program need not do anything about 
it. [In fact I think the program becomes erroneous - which isn't really 
very useful.]

Probably of more use is the Technical Report currently being written by 
the Annex H Rapporteur Group (the HRG - a subgroup of WG9). This is 
titled (something like) "Guidance on the use of the Ada language for 
high-integrity software" and a preliminary draft has recently been 
circulated within the HRG mailing list for comment. There is another 
meeting of the Group in a couple of weeks to review comments received 
and I think the plan is that the draft resulting from that meeting is to 
be published in Ada Letters later this year. [Once the report is 
formally circulated within ISO then I believe that copyright 
restrictions will prevent it being published elsewhere.]

This report has very little to say about Annex H, but concentrates on 
the links between the features of the language and how the various 
verification and validation techniques are affected by their use.

The other excellent reference in this area is John Barnes' book: High 
Integrity Ada, The SPARK Approach, but that makes no reference to
Annex H at all.

Phil Thornley

-- 
------------------------------------------------------------------------
| JP Thornley    EMail jpt@diphi.demon.co.uk                           |
|                      phil.thornley@acm.org                           |
------------------------------------------------------------------------