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=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,323f382d1271f5b6 X-Google-Attributes: gid103376,public From: jpt@diphi.demon.co.uk (JP Thornley) Subject: Re: Safety Critical Systems and Ada 95 Date: 1998/06/10 Message-ID: <485015649wnr@diphi.demon.co.uk>#1/1 X-Deja-AN: 361454686 References: <357EB552.5CF3EB9@swl.msd.ray.com> X-Complaints-To: abuse@demon.net X-Mail2News-Path: news.demon.net!post-20.mail.demon.net!post.mail.demon.net![158.152.212.133] X-Trace: mail2news.demon.co.uk 897507075 mail2news:17045 mail2news mail2news.demon.co.uk Organization: None Reply-To: jpt@diphi.demon.co.uk Newsgroups: comp.lang.ada Date: 1998-06-10T00:00:00+00:00 List-Id: In article: <357EB552.5CF3EB9@swl.msd.ray.com> "John J Cupak Jr, CCP" 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 | ------------------------------------------------------------------------