Communicating between in and out contracts

[Andrei Alexandrescu]

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