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.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,74b55538385b7366 X-Google-Attributes: gid103376,public From: Peter Amey Subject: Re: Ada safety road Was: Which is right ... Date: 1999/06/10 Message-ID: <375F6F0B.AD735B5B@praxis-cs.co.uk>#1/1 X-Deja-AN: 487824740 Content-Transfer-Encoding: 7bit References: <928083159.436.79@news.remarQ.com> <928174549.336.98@news.remarQ.com> <7iuqkc$ln6$1@nnrp1.deja.com> <928529202.956.79@news.remarQ.com> <928569312.951.42@news.remarQ.com> <7jb1l9$694$1@nnrp1.deja.com> <928703068.617.98@news.remarQ.com> X-Accept-Language: en Content-Type: text/plain; charset=us-ascii X-Complaints-To: abuse@uk.uu.net X-Trace: soap.pipex.net 929001487 9598 194.129.236.147 (10 Jun 1999 07:58:07 GMT) Organization: Praxis Critical Systems Mime-Version: 1.0 NNTP-Posting-Date: 10 Jun 1999 07:58:07 GMT Newsgroups: comp.lang.ada Date: 1999-06-10T07:58:07+00:00 List-Id: Vladimir Olensky wrote: > > Robert Dewar wrote in message <7jb1l9$694$1@nnrp1.deja.com>... > > >And to repeat, since you keep repeating the subject, both > >GNAT and OA are right here, and do what the RM intends! > > Sorry, It just didn't come up to my mind to change the subject. > Even original subject was not very adequate to what I had in mind > I really did not had intention on insisting which is better in following RM. > > I had other things in mind. > > I was just thinking about different aspects of providing some > general kind of "foolproofness" to program written in Ada in places where RM > define program behavior as erroneous. > I think nobody would like to be on a plane that performed erroneous flight > """' ' ' ^~\_+. > Anyone would prefer to be accidentally on board of the wrong flight instead. > > One good aspect of Ada is that when it is impossible to provide compiler > solution to some problems (due to implementation cost and some other reasons > that may not be very obvious) LRM at least honestly specifies situations > when erroneous execution is possible. > > But I see one problem here. All this information is scattered around RM. > > I think that to facilitate safety programming such info should be gathered > into one paper > with explanations why it was not possible to overcome such situations and > it should contain many examples covering different aspects that leads to > erroneous execution. There should be no indirect references ("other then > ...."). Everything should be directly described and should be as simple as > possible. > I see it as some kind of "Ada safety programming roadmap". And of course > such paper should be easily available online for all interested in it. So > far I have not seen such document available online . > If you crossing mine field and you do not have good map with red marks on it > all your life depends on your luck :-) > Such type of documents are usually top level documents in design of any > safety critical system (at least it was in my experience). > [snip] > Regards, > > Vladimir Olensky There certainly has been some work in this area. At a pragmatic level there is the Ada HRG which has produced (under auspices of ISO) a guidance document on the use of Ada in high-intergrity systems. The document identifies language features and combinations of features which are most likely to complicate reasoning about the behaviour of Ada programs; clearly this includes behaviour which might be erroneous. At a more rigorous level, the SPARK language makes it possible to construct programs which can be shown, prior to execution, to be free from _any_ erroneous behaviour; this includes proving that the program will not raise any predefined exceptions. Peter -- --------------------------------------------------------------------------- __ Peter Amey, Product Manager ) Praxis Critical Systems Ltd / 20, Manvers Street, Bath, BA1 1PX / 0 Tel: +44 (0)1225 466991 (_/ Fax: +44 (0)1225 469006 http://www.praxis-cs.co.uk/ --------------------------------------------------------------------------