Re: Ada safety road Was: Which is right ...

[Peter Amey <pna@praxis-cs.co.uk>]

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/

--------------------------------------------------------------------------