From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,c4190027f6de5b93 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-02-05 01:02:16 PST Path: supernews.google.com!sn-xit-02!supernews.com!news.tele.dk!130.133.1.3!fu-berlin.de!uni-berlin.de!193.114.91.187!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: Computation of exception handling Date: Mon, 05 Feb 2001 09:02:03 +0000 Organization: Praxis Critical Systems Message-ID: <3A7E6C0B.5DF54BA@praxis-cs.co.uk> References: <94jr16$j2q$1@nnrp1.deja.com> <94ki0n$j4d$1@usenet.rational.com> <3a6ef4d9$1@pull.gecm.com> <3a7188ec$1@pull.gecm.com> <94s4ov$qfo$1@nnrp1.deja.com> <3A7316F6.87EDF50B@ntlworld.com> <3A753496.67442B90@praxis-cs.co.uk> <955n83$cjr$1@nnrp1.deja.com> <3a768497$1@pull.gecm.com> NNTP-Posting-Host: 193.114.91.187 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: fu-berlin.de 981363734 18070020 193.114.91.187 (16 [69815]) X-Mailer: Mozilla 4.73 [en] (WinNT; U) X-Accept-Language: en Xref: supernews.google.com comp.lang.ada:4934 Date: 2001-02-05T09:02:03+00:00 List-Id: 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 ; successful : out boolean) is > -- exceptions not allowed here > begin > -- exceptions allowed from here > successful := true; > -- exceptions not allowed from here > exception > when => > -- exceptions not allowed here > value := > successful := false; > end blah; > > Robert Dewar wrote in message > news:955n83$cjr$1@nnrp1.deja.com... > > In article <3A753496.67442B90@praxis-cs.co.uk>, > > Peter Amey 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/ --------------------------------------------------------------------------