Communicating between in and out contracts

[Rainer Deyke]

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.


-- 
Rainer Deyke - rainerd at eldwood.com