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: 103376,c80e6f742e73478f
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!q21g2000yqm.googlegroups.com!not-for-mail
From: AdaMagica <christoph.grein@eurocopter.com>
Newsgroups: comp.lang.ada
Subject: Re: Ensuring postconditions in the face of exceptions
Date: Mon, 15 Mar 2010 04:04:51 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <cf793da4-833e-4fd3-a083-5f209eef47a4@q21g2000yqm.googlegroups.com>
References: 
 <820d96c0-5d67-4b8c-8c5b-811ca4f1127e@g26g2000yqn.googlegroups.com>
NNTP-Posting-Host: 80.156.44.178
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1268651092 32616 127.0.0.1 (15 Mar 2010 11:04:52
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 15 Mar 2010 11:04:52 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: q21g2000yqm.googlegroups.com; posting-host=80.156.44.178;
	posting-account=rmHyLAoAAADSQmMWJF0a_815Fdd96RDf
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.1; SV1;
 .NET
	CLR 1.1.4322; .NET CLR 2.0.50727; InfoPath.1; .NET CLR 3.0.04506.30;
 .NET CLR
	3.0.4506.2152; .NET CLR 3.5.30729),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:10542
Date: 2010-03-15T04:04:51-07:00
List-Id: <comp.lang.ada>

> generic
> =A0 =A0with procedure Visit (Object : in out T);
> procedure Refresh (Object : in out T; Dirty : access Boolean) is
> begin
> =A0 =A0if Dirty then
> =A0 =A0 =A0 Visit (Object);
> =A0 =A0 =A0 Dirty :=3D False;
> =A0 =A0end if;
> exception
> =A0 =A0when others =3D>
> =A0 =A0 =A0 Dirty :=3D True; -- warnings here
> =A0 =A0 =A0 raise;
> end Refresh;

This is the proposed solution, I guess. I've got problems with this.
As fas as I understand the RM, the compiler is free to replace a
complete block of code by just raising the exception if it can prove
that the exception will be raised.

So how then can you be sure that the parameter Dirty is set as you
expect? An exception is an exceptional case (say what!), so I do not
see how you can define normal postconditions for any parameters
(scalars don't work as the compiler has told you - and for others, see
above).