Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!batcomputer!munnari.oz.au!metro!usage.csd.unsw.oz.au!syacus!ian
From: ian@syacus.acus.oz.au (Ian Joyner)
Newsgroups: comp.lang.eiffel
Subject: Old confusion
Summary: A question on the semantics of old is asked
Keywords: old, ensure, postconditions
Message-ID: <1991May21.040742.1520@syacus.acus.oz.au>
Date: 21 May 91 04:07:42 GMT
Distribution: comp
Organization: ACUS Australian Centre for Unisys Software, Sydney
Lines: 36

Paulo Barreto asked the following question on an internal Unisys newsgroup,
and as he does not have access to the InterNet, I agreed to post it here
for him.

>
I'd like to know what should an Eiffel compiler do when it finds two or
more occurences of the same call preceded by "old" within an assertion.

If that call produces side effect, the values of these occurences may
be different. For instance:

class TROUBLE
export headache
feature
	aux: INTEGER;
	
	puzzle: INTEGER is
		do
			Result := aux;
			aux := aux + 1;  -- side effect!
		end; -- puzzle

	headache is
		ensure
			old puzzle = old puzzle -- what now
		end -- headache
end -- class TROUBLE
<

I already responded to Paulo, what I thought the answer was, although,
I wasn't certain. I will forward any responses to him. Thanks.

-- 
Ian Joyner                                     ACSNet: ian@syacus.oz
ACUS (Australian Centre for Unisys Software)   DNS:  ian@syacus.oz.au
Tel 61-2-390 1328      Fax 61-2-390 1391       UUCP: ...uunet!munnari!syacus.oz