* Re: Computation of exception handling [not found] ` <3a7188ec$1@pull.gecm.com> @ 2001-01-26 20:12 ` Florian Weimer [not found] ` <94s4ov$qfo$1@nnrp1.deja.com> 2001-01-28 7:35 ` Simon Wright 2 siblings, 0 replies; 9+ messages in thread From: Florian Weimer @ 2001-01-26 20:12 UTC (permalink / raw) "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.) ^ permalink raw reply [flat|nested] 9+ messages in thread
[parent not found: <94s4ov$qfo$1@nnrp1.deja.com>]
* Re: Computation of exception handling [not found] ` <94s4ov$qfo$1@nnrp1.deja.com> @ 2001-01-27 18:44 ` martin.m.dowie 2001-01-29 9:15 ` Peter Amey 0 siblings, 1 reply; 9+ messages in thread From: martin.m.dowie @ 2001-01-27 18:44 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Computation of exception handling 2001-01-27 18:44 ` martin.m.dowie @ 2001-01-29 9:15 ` Peter Amey 2001-01-30 6:33 ` Robert Dewar 0 siblings, 1 reply; 9+ messages in thread From: Peter Amey @ 2001-01-29 9:15 UTC (permalink / raw) "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/ -------------------------------------------------------------------------- ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Computation of exception handling 2001-01-29 9:15 ` Peter Amey @ 2001-01-30 6:33 ` Robert Dewar 2001-01-30 9:15 ` Martin Dowie 0 siblings, 1 reply; 9+ messages in thread From: Robert Dewar @ 2001-01-30 6:33 UTC (permalink / raw) 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/ ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Computation of exception handling 2001-01-30 6:33 ` Robert Dewar @ 2001-01-30 9:15 ` Martin Dowie 2001-02-05 9:02 ` Peter Amey 0 siblings, 1 reply; 9+ messages in thread From: Martin Dowie @ 2001-01-30 9:15 UTC (permalink / raw) 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/ ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Computation of exception handling 2001-01-30 9:15 ` Martin Dowie @ 2001-02-05 9:02 ` Peter Amey 2001-02-05 12:19 ` Martin Dowie 0 siblings, 1 reply; 9+ messages in thread From: Peter Amey @ 2001-02-05 9:02 UTC (permalink / raw) 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/ -------------------------------------------------------------------------- ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Computation of exception handling 2001-02-05 9:02 ` Peter Amey @ 2001-02-05 12:19 ` Martin Dowie 0 siblings, 0 replies; 9+ messages in thread From: Martin Dowie @ 2001-02-05 12:19 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Computation of exception handling [not found] ` <3a7188ec$1@pull.gecm.com> 2001-01-26 20:12 ` Computation of exception handling Florian Weimer [not found] ` <94s4ov$qfo$1@nnrp1.deja.com> @ 2001-01-28 7:35 ` Simon Wright 2 siblings, 0 replies; 9+ messages in thread From: Simon Wright @ 2001-01-28 7:35 UTC (permalink / raw) "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 ... ^ permalink raw reply [flat|nested] 9+ messages in thread
[parent not found: <94mgqh$suo$1@nnrp1.deja.com>]
* Re: Computation of exception handling [not found] ` <94mgqh$suo$1@nnrp1.deja.com> @ 2001-02-02 22:17 ` Mark Lundquist 0 siblings, 0 replies; 9+ messages in thread From: Mark Lundquist @ 2001-02-02 22:17 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2001-02-05 12:19 UTC | newest] Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- [not found] <94jr16$j2q$1@nnrp1.deja.com> [not found] ` <94ki0n$j4d$1@usenet.rational.com> [not found] ` <gauthier-2401011437350001@193.50.185.13> [not found] ` <3a6ef4d9$1@pull.gecm.com> [not found] ` <gauthier-2601011508270001@193.50.185.13> [not found] ` <3a7188ec$1@pull.gecm.com> 2001-01-26 20:12 ` Computation of exception handling Florian Weimer [not found] ` <94s4ov$qfo$1@nnrp1.deja.com> 2001-01-27 18:44 ` martin.m.dowie 2001-01-29 9:15 ` Peter Amey 2001-01-30 6:33 ` Robert Dewar 2001-01-30 9:15 ` Martin Dowie 2001-02-05 9:02 ` Peter Amey 2001-02-05 12:19 ` Martin Dowie 2001-01-28 7:35 ` Simon Wright [not found] ` <94mgqh$suo$1@nnrp1.deja.com> 2001-02-02 22:17 ` Mark Lundquist
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox