Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!pyrltd!tetrauk!rick
From: rick@tetrauk.UUCP (Rick Jones)
Newsgroups: comp.lang.eiffel
Subject: Re: Old confusion
Keywords: old, ensure, postconditions
Message-ID: <1166@tetrauk.UUCP>
Date: 22 May 91 09:59:56 GMT
References: <1991May21.040742.1520@syacus.acus.oz.au>
Reply-To: rick@tetrauk.UUCP (Rick Jones)
Distribution: comp
Organization: Tetra Ltd., Maidenhead, UK
Lines: 40

In article <1991May21.040742.1520@syacus.acus.oz.au> ian@syacus.acus.oz.au (Ian Joyner) writes:
>Paulo Barreto asked the following question:
>>
>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. [ example deleted ]

This is really an issue of application design, and is beyond the control of the
compiler.  The Eiffel "philosophy" is that routines should be either functions
or procedures;  i.e. a routine which returns a value is a function, and should
always be written without side effects.  It can therefore be called repeatedly
without changing the state of the system.  A procedure which does change the
state should not have a return value.

The compiler can never totally enforce this, although it does produce warnings
if you call a function and don't assign its return value.  (If it is a true
function without side-effects the statement is pointless, if the statement is
not pointless the routine must change the state so it should not have a return
value.)  I must confess that I sometimes break this rule, but only to the
extent of having a procedure return a boolean to indicate whether it succeeded
or not - and such routines would have no value in as assertion statment.

The use of function calls within assertions is one particular reason for
observing this rule.  This is essential regardless of whether "old" is used,
since the presence of an assertion should never change the semantics of the
application.  If an assertion calls any function which has a side effect, then
the application will behave differently depending on whether assertions are
enabled or not.  This is clearly a situation to avoid!

I believe the compiler should be free to assume that functions do not have side
effects.  If you write functions with side effects and then use them in
assertions, you are on your own.

-- 
Rick Jones, Tetra Ltd.  Maidenhead, Berks, UK
rick@tetrauk.uucp

Any fool can provide a solution - the problem is to understand the problem