Communicating between in and out contracts

[Andrei Alexandrescu]

Rainer Deyke wrote:
> Andrei Alexandrescu wrote:
>> Rainer Deyke wrote:
>>> Also, from the Eiffel docs
>>> (http://archive.eiffel.com/doc/online/eiffel50/intro/language/invitation-07.html):
>>>
>>>   The notation 'old  expression' is only valid in a routine
>>> postcondition. It denotes the value the expression had on routine entry.
>>>
>>> It seems that Eiffel had 'old' semantics that I've proposed all along.
>> Great. Others brought it up too, inspired from Eiffel.
>>
>>> Any significant problems with this approach would have been discovered
>>> by the Eiffel community by now.
>> There is no problem if a copy of the object is made upon entry in the
>> procedure. That's what I think Eiffel does. I was hoping to avoid that
>> by allowing the "out" contract to see the definitions in the "in" contract.
> 
> 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?

Andrei