Andrei Alexandrescu wrote: > Rainer Deyke wrote: >> Copying the object would be completely broken, so I'm sure that that's >> *not* how Eiffel does it. "It denotes the value the expression had on >> routine entry." In other words, the expression is evaluated once, on >> routine entry, and the result is cached for use in the postcondition. > > What if the expression is conditioned by the new state of the object?
Not allowed. Since 'old(x)' is the value of 'x' evaluated at the beginning of the function, it must be possible to evaluate 'x' at the beginning of the function. Either rewrite the assertion or drop it. I have a feeling that this will only rarely be an issue. -- Rainer Deyke - rain...@eldwood.com
