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-Thread: a07f3367d7,c80e6f742e73478f X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news2.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nntp.club.cc.cmu.edu!elk.ncren.net!newsswitch.lcs.mit.edu!nntp.TheWorld.com!not-for-mail From: Robert A Duff Newsgroups: comp.lang.ada Subject: Re: Ensuring postconditions in the face of exceptions Date: Sun, 14 Mar 2010 11:38:38 -0400 Organization: The World Public Access UNIX, Brookline, MA Message-ID: References: <820d96c0-5d67-4b8c-8c5b-811ca4f1127e@g26g2000yqn.googlegroups.com> <8990d686-f703-4e9c-91b7-32410289983d@g11g2000yqe.googlegroups.com> <87ljdv56gy.fsf@ludovic-brenta.org> NNTP-Posting-Host: shell01.theworld.com Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: pcls6.std.com 1268581100 13726 192.74.137.71 (14 Mar 2010 15:38:20 GMT) X-Complaints-To: abuse@TheWorld.com NNTP-Posting-Date: Sun, 14 Mar 2010 15:38:20 +0000 (UTC) User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix) Cancel-Lock: sha1:FwdRRM0/aj2OZlNT4G2Y3ZGgSaQ= Xref: g2news2.google.com comp.lang.ada:10534 Date: 2010-03-14T11:38:38-04:00 List-Id: Ludovic Brenta writes: > That's an interesting suggestion but we've patched the run-time library > so that it dumps core on every exception;... Then how can it ever get to the "when others" in Refresh? Or do you mean it dumps core, and then the program continues on past the point of the bug (propagates the exception, handles it, etc)? Is "dirty" a property of the object being visited? If so, would it make sense to make it a component of that object, and make sure that is passed by reference (either by explicitly passing a pointer, or by making the type limited or tagged)? By the way, I think it makes perfect sense to have different postconditions for normal return, and for each exception that might be raised. - Bob