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-01-29 01:15: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, 29 Jan 2001 09:15:02 +0000 Organization: Praxis Critical Systems Message-ID: <3A753496.67442B90@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> 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 980759708 15537962 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:4647 Date: 2001-01-29T09:15:02+00:00 List-Id: "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/ --------------------------------------------------------------------------