Re: Computation of exception handling

Re: Computation of exception handling

[Florian Weimer]

"Martin Dowie" <martin.dowie@gecm.com> writes:

> > There is nothing wrong. This is _strictly_ equivalent to raising
> > an exception with the same identifier, at least at formal level.
> > The difference is _strictly_ syntactic. More often, the program is
> > simply less complex with exceptions that with report codes.

> but you can't use exceptions if your system has to be 'safe' (no
> mention of that in the original question).

The problem without exceptions is that people forget to check for
error conditions.  (C programmers using the POSIX API make this
mistake quite often.)

Re: Computation of exception handling

[martin.m.dowie]

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?


Robert Dewar wrote:

> This is only true if the definition of 'safe' arbitrarily
> says that exceptions are not allowed, in which case it is
> simply restating this definition.
>
> There is no technical principle that makes exceptions
> inherently unsafe in any reasonable technical meaning
> of the term.

Re: Computation of exception handling

[Peter Amey]

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

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

Re: Computation of exception handling

[Robert Dewar]

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/

Re: Computation of exception handling

[Martin Dowie]

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/

Re: Computation of exception handling

[Peter Amey]

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/

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

Re: Computation of exception handling

[Martin Dowie]

Thanks for the reply - I'm one of those waiting for the ravenscar support
:-)

Peter Amey <pna@praxis-cs.co.uk> wrote in message
news:3A7E6C0B.5DF54BA@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

Re: Computation of exception handling

[Simon Wright]

"Martin Dowie" <martin.dowie@gecm.com> writes:

> but you can't use exceptions if your system has to be 'safe' (no
> mention of that in the original question).

You can't use exceptions if your independent safety assessor wants you
to use a code analysis tool set that doesn't support them. Or tasks,
or tagged tyoes, or generics, or ...

Re: Computation of exception handling

[Mark Lundquist]

Hi again Sandro...

Sandro Binetti <sandrobinetti@yahoo.com> wrote in message
news:94mgqh$suo$1@nnrp1.deja.com...

>
> Do you think I'm using exception handling in an uncorrect way?
> How "exceptional" has to be an event, if occurs, to be
> considered "algoritmically treated", instead of "exception handled"?
> --
> Bye, Sandro

I would say:

If you depend on exception handleing being fast, this is an implementation
dependency.

If after that, exceptions are still an option for you, then use them if in
your judgement it makes the code easier to understand (or at least, no
harder).  If it's a just a notational shortcut that makes it easier to write
but harder to understand, then I wouldn't use them.  But there's nothing
wrong with making it easier to write if it doesn't obscure the code.  Maybe
it makes it easier to write *and* read -- if so, great, use 'em!

-- mark