Re: Computation of exception handling

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

It certainly looks ok at first glance.  The difficulty from our point of
view is that it is usually very easy to come up with examples of safe
use of almost any language feature.  (Robert is fond of pointing out how
useful goto can be if used sensibly).  From the SPARK design point of
view the problem is not showing that something can be safely used but
showing that there is _no_ way of using that creates ambiguous
behaviour.  We are in the "for all constructs no ambiguity" rather than
"there exists a safe use" territory!

I am sure that we could come up with something for local exception
handling; however, feedback from users suggests that this is much less
important than the things we are doing to support "abstract oriented
programming" such as the INFORMED design methods, using annotations to
bind _system_ and _software_ designs, proof of programs involving
abstract state and support for Ravenscar.

Peter

Martin Dowie wrote:
> 
> so could the following template be described as 'safe'? i.e. limit the
> 'allowable' use of exceptions situation where they never propagate?
> 
> procedure blah (value : out <some_type>; successful : out boolean) is
>   -- exceptions not allowed here
> begin
>   -- exceptions allowed from here
>   successful := true;
>   -- exceptions not allowed from here
> exception
>   when <exception_name> =>
>     -- exceptions not allowed here
>     value := <known_safe value>
>     successful := false;
> end blah;
> 
> Robert Dewar <robert_dewar@my-deja.com> wrote in message
> news:955n83$cjr$1@nnrp1.deja.com...
> > In article <3A753496.67442B90@praxis-cs.co.uk>,
> >   Peter Amey <pna@praxis-cs.co.uk> wrote:
> > > One of the main reasons SPARK does not support exceptions is
> > > that we wanted a language free from implementation
> > > dependencies.
> >
> > I don't see any unsurmountable obstacle in defining extensions
> > to SPARK that would allow exceptions to be raised without
> > creating any implementation defined unknown situations. Yes
> > you would have to limit what can be done in exception handlers,
> > but SPARK is in the business of figuring out appropriate
> > restrictions :-)
> >
> >
> > Sent via Deja.com
> > http://www.deja.com/

-- 
---------------------------------------------------------------------------   
      __         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/

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