Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!jarthur!nntp-server.caltech.edu!tll
From: tll@nntp-server.caltech.edu (Tal Lewis Lancaster)
Newsgroups: comp.lang.eiffel
Subject: Re: Old confusion
Keywords: old, ensure, postconditions
Message-ID: <1991May21.171225.12321@nntp-server.caltech.edu>
Date: 21 May 91 17:12:25 GMT
References: <1991May21.040742.1520@syacus.acus.oz.au>
Distribution: comp
Organization: California Institute of Technology, Pasadena
Lines: 66

ian@syacus.acus.oz.au (Ian Joyner) writes:

>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

		-- this needs some kind of body to even compile

>		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.

First, this example is a good one for showing how to not program in
Eiffel.  It is also shows why it is bad to have functions with
side-effects.  Assuming headache was given a body and CHECK_ALL_ASSERTIONS
flag has been turn on for the class, headache would trigger an EXCEPTION
and the routine will fail when it is called.  However if the class
didn't have assertion monitoring on the ensure statement will never
be executed.

It may be interesting to note that in Version 3, the above ensure statement
is syntatically incorrect

Expression -is defined as- Standard_expression | Old_expression

Old_expression -is defined as- old Standard_expression

Before these were:

Expression -is defined as- Constant | Call | Operator_expression |
				Current | Old_value | Nochange

Old_value -is defined as- old Expression

>-- 
>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


Tal Lancaster