Xref: utzoo comp.object:3696 comp.lang.eiffel:1651
Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!uunet!mcsun!ukc!pyrltd!tetrauk!rick
From: rick@tetrauk.UUCP (Rick Jones)
Newsgroups: comp.object,comp.lang.eiffel
Subject: Re: Functions without side effects (was Old confusion)
Message-ID: <1186@tetrauk.UUCP>
Date: 12 Jun 91 10:14:36 GMT
References: <130242@tut.cis.ohio-state.edu> <1991Jun5.072556.19870@irisa.fr> <1991Jun5.083241.13145@tkou02.enet.dec.com> <956@puck.mrcu>
Reply-To: rick@tetrauk.UUCP (Rick Jones)
Organization: Tetra Ltd., Maidenhead, UK
Lines: 22

In article <956@puck.mrcu> paj@uk.co.gec-mrc (Paul Johnson) writes:
>
>Why not add a keyword `unchanged' to the `ensure' clause?  This would
>be equivalent to something along the lines of `current.equal( old
>current )' and would assert that the function has not changed
>anything.

Wait for Eiffel version 3! (not long now, I hope).  It will support a construct
"strip" which means "the attributes of this object, except for <the parameters
given to strip>".  If there are no parameters, it is all the attributes.  Then
the postcondition "strip = old strip" means "no change".  Since strip allows
you to explicitly omit specified attributes, you can write a postcondition
which means "no change to any attributes except those specified".  So by
omitting attributes which only affect internal state, the postcondition can
ensure that the important things are unchanged, even though the internal state
may have been modified.

-- 
Rick Jones, Tetra Ltd.  Maidenhead, Berks, UK		rick@tetrauk.uucp
Chairman, NICE (Non-profit International Consortium for Eiffel)

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