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
