Communicating between in and out contracts

Andrei Alexandrescu SeeWebsiteForEmail at erdani.org
Sat Oct 17 15:00:54 PDT 2009


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




More information about the Digitalmars-d mailing list