Communicating between in and out contracts

[Rainer Deyke]

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 - rainerd at eldwood.com