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 04:23:42 PST
From: "Martin Dowie" <martin.dowie@gecm.com>
Newsgroups: comp.lang.ada
References: <94jr16$j2q$1@nnrp1.deja.com> <94ki0n$j4d$1@usenet.rational.com>
 <gauthier-2401011437350001@193.50.185.13> <3a6ef4d9$1@pull.gecm.com>
 <gauthier-2601011508270001@193.50.185.13> <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> <3A7E6C0B.5DF54BA@praxis-cs.co.uk>
Subject: Re: Computation of exception handling
Date: Mon, 5 Feb 2001 12:19:41 -0000
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 5.00.2314.1300
X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2314.1300
NNTP-Posting-Host: superted.dsge.edinbr.gmav.gecm.com
Message-ID: <3a7e98d8$1@pull.gecm.com>
X-Trace: 5 Feb 2001 12:13:12 GMT, superted.dsge.edinbr.gmav.gecm.com
Path: 
 supernews.google.com!sn-xit-02!supernews.com!news.tele.dk!193.190.198.17!newsfeeds.belnet.be!news.belnet.be!btnet-peer1!btnet-feed5!btnet!newreader.ukcore.bt.net!pull.gecm.com!superted.dsge.edinbr.gmav.gecm.com
Xref: supernews.google.com comp.lang.ada:4936
Date: 2001-02-05T12:19:41+00:00
List-Id: <comp.lang.ada>

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