Rainer Deyke wrote:
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.
If x is a complex expression and part of a complex control flow, it
becomes highly difficult what it means "at the beginning of the
function". It also becomes difficult to find a way to distinguish good
cases from bad cases without being overly conservative.
I have no idea how Eiffel pulls it off.
Andrei
