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,a00006d3c4735d70
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2004-02-03 00:46:31 PST
Path: 
 archiver1.google.com!news2.google.com!fu-berlin.de!uni-berlin.de!tar-atanamir.cbb-automation.DE!not-for-mail
From: Dmitry A. Kazakov <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: In-Out Parameters for functions
Date: Tue, 03 Feb 2004 09:54:40 +0100
Message-ID: <16nu1099ekujjbpe9dqvs3noi9sdcfja6e@4ax.com>
References: <1075303237.975898@master.nyc.kbcfp.com>
 <9khh10pti0dn8gcp7f18ghptaifluj0fud@4ax.com>
 <1075390647.405841@master.nyc.kbcfp.com>
 <pan.2004.01.29.18.20.03.61778@email.ro>
 <1075405582.982776@master.nyc.kbcfp.com>
 <s06k109c4nesjr09rhtilrh1ksjsanl6cs@4ax.com>
 <1075482385.142744@master.nyc.kbcfp.com>
 <tk3s10lso10c53841dr3sk5kiok5p46gjf@4ax.com>
 <1075732402.294581@master.nyc.kbcfp.com>
 <loqs105qi5ud0uhet3vbjinlhknmaf4o40@4ax.com>
 <1075741279.952497@master.nyc.kbcfp.com>
NNTP-Posting-Host: tar-atanamir.cbb-automation.de (212.79.194.116)
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Trace: news.uni-berlin.de 1075797989 31704269 212.79.194.116 ([77047])
X-Newsreader: Forte Agent 1.8/32.548
Xref: archiver1.google.com comp.lang.ada:5196
Date: 2004-02-03T09:54:40+01:00
List-Id: <comp.lang.ada>

On Mon, 02 Feb 2004 12:01:19 -0500, Hyman Rosen <hyrosen@mail.com>
wrote:

>Dmitry A. Kazakov wrote:
>> Semantically wrong code cannot be made correct by doing that.
>
>That's not true. If it happens that a defined evaluation order
>would do what the programmer wanted, then the code would indeed
>become correct.

I do not think so. + is commutative, if a programmer uses it so that
a+b /= b+a, he makes a semantical error. Later on, he may forget about
his mistake, a code viewer will be even not aware about it. So I treat
it as a *wrong* code. A wrong code may under some circumstances
function properly, false => true. You want to fix the circumstances, I
prefer to fix the code.

>> it is like to define the result of A [-99999999999] as 0
>
>No, it's not nearly as bad, because in the case of evaluation order,
>we are specifying one of a set of legal results, whereas for indexing
>there is no legal result.

The results are illegal, if different [*]. When a programmer writes:
x:=a+b, the postcondition of that is:

{ x=a+b & x=b+a }

so there is no legal way to make it dependent on the evaluation order.

>> Wrong code should not go so far.
>
>But there is (nearly) nothing to be gained by forcing the code to be
>considered wrong.

Yes, if that cannot be checked. As I always said, I wished to have
pure functions in Ada.

------
* Floating point numbers are intervals and equations become inclusions
and the postcondition will hold.

--
Regards,
Dmitry A. Kazakov
www.dmitry-kazakov.de