Re: Computation of exception handling

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

"martin.m.dowie" wrote:
> 
> i've yet to come across any definitions of a safe subset of Ada that
> don't exclude exceptions - do you know of any, or are they normally
> excluded because it makes life (much) easier from a proof/certification
> stand point?
> 

One of the main reasons SPARK does not support exceptions is that we
wanted a language free from implementation dependencies.  If you allow
an exception to propagate then, at the point where you eventually try
and handle it, the system is in an "unknown" (or at least
"implementation-defined") state.  For example, if your compiler passes
subprogram parameters by copy-in, copy-out and an exception is raised
part way through a subprogram then any changes to those parameters will
not get propagated back to the system state; however, if the compiler
passes parameters by reference then the changes will already have
affected the system's state when the exception is raised.  I have always
considered that the chances of writing code that correctly deals with
exceptional situations in a system of unknown state to be relatively
small :-)  It might be possible to reason about exceptions locally but
propogation causes real difficulties.  

BTW, we don't just wash our hands of this: SPARK does provide a
straightforward way of proving that code 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/

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