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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b3f788f59498d3af X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news4.google.com!feeder1-2.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Exceptions and out procedure arguments (using GNAT GPL) Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <79c673pq5htg508nkoi935n3udqg5ps7r8@4ax.com> <1182181497.595409.300500@a26g2000pre.googlegroups.com> <1182238493.512406.168820@o61g2000hsh.googlegroups.com> <1182266486.650797.262430@a26g2000pre.googlegroups.com> <4678c6a0$0$23135$9b4e6d93@newsspool1.arcor-online.net> <1o6rnwgzezcr2$.mv31ct5mmmso$.dlg@40tude.net> <1182329193.7759.30.camel@kartoffel> <1182334409.7759.39.camel@kartoffel> <1mhmyqf4l1lzn$.42eeylu5yrjk.dlg@40tude.net> <1182349018.7759.51.camel@kartoffel> <1d3hk782jujgz$.182e58lrsup7s.dlg@40tude.net> <46797c40$0$23133$9b4e6d93@newsspool1.arcor-online.net> <1182419529.23934.17.camel@kartoffel> <1lyxtgyzyuh8m.yvrov7e73y09.dlg@40tude.net><467c10e5$0$14879$9b4e6d93@newsspool4.arcor-online.net> Date: Fri, 22 Jun 2007 21:45:20 +0200 Message-ID: <15wdv3qz51cqd$.pl6zy4m98ojn$.dlg@40tude.net> NNTP-Posting-Date: 22 Jun 2007 21:44:58 CEST NNTP-Posting-Host: a8c949b1.newsspool4.arcor-online.net X-Trace: DXC=^ZHjGHeKH?VV0Pe9PRnbJ\4IUK On Fri, 22 Jun 2007 20:15:02 +0200, Georg Bauhaus wrote: > Dmitry A. Kazakov wrote: >> >> I didn't talk about formal correctness or pre-/postconditions, but if you >> bring this topic in. What is so difficult in: > > I had this in mind: > "Actually I think that boils down to your [Adam Beneschan's] stand point > on exceptions vs. program correctness. Mine is that any exception shall > be a valid (correct) outcome. > > "In other words, exceptions are a subject of DbC, they aren't a vehicle of. " > > How, exactly, can exception be made a subject of DbC (other than > banning them)? By having contracted exceptions, obviously. Heck, I am not an employee of Praxis, you know, so you'd better ask them. But if I were at their place, I would introduce the predicate propagated(e). For each e, exception, propagated(e) is true when e is being propagated. Trivially, each Ada statement has in its precondition forall e not propagated (e) except for the first statement of an exception handler: exception when Constraint_Error => require propagated(Constraint_Error) and not (...other exceptions...); For built-in operations like "+" we could have: function "+" (Left, Right : Integer) return Integer; ensure (Left + Right not in Integer'Range and propagated(Constraint_Error)) or (Left + Right in Integer'Range and Result = Left + Right) [and not propagated (Program_Error) and not propagated (Data_Error) ...)] For raise: raise e; ensure propagated(e) [and not ...] P.S. Robert Duff said on many occasions that Storage_Error could be propagated almost anywhere. That's better to change and he mentioned some ideas of how to do this. But Storage_Error is not a catastrophe for provability. Just don't mention it in the contracts, and *consequently* don't handle it because you could not. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de