Communicating between in and out contracts

[Andrei Alexandrescu]

Walter Bright wrote:
> Rainer Deyke wrote:
>> Andrei Alexandrescu wrote:
>>> Eiffel offers the "old" keyword that refers to the old object in a
>>> postcondition. But it seems quite wasteful to clone the object just to
>>> have a contract look at a little portion of the old object.
>>
>> You don't need to clone the whole object.  You just need to cache the
>> properties that are used with 'old'.
> 
> That's a good idea.

Should work, but it has more than a few subtleties. Consider:

class A {
     int fun() { ... }
     int gun(int) { ... }

     int foo()
     in {
     }
     out(result) {
         if (old.fun())
            assert(old.gun(5));
         else
            assert(old.fun() + old.gun(6));
         foreach (i; 1 .. old.fun())
            assert(gun(i * i));
     }
     ...
}

Now please tell what's cached and in what order.


Andrei