Communicating between in and out contracts

[Andrei Alexandrescu]

Rainer Deyke wrote:
> Rainer Deyke wrote:
>> Andrei Alexandrescu wrote:
>>> I honestly believe the whole "old" thing can't be made to work. Shall we
>>> move on to other possibilities instead of expending every effort on
>>> making this bear dance?
>> It definitely /can/ be made to work, for some value of "work".  It
>> sacrifices the natural order of evaluation to gain a concise and
>> intuitive syntax.  I don't think it should be dismissed out of hand.
> 
> 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.


Andrei