Communicating between in and out contracts

[Jason House]

Andrei Alexandrescu Wrote:

> 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

if fun or gun is impure, then they should not be callable by the contracts. Because of that, order is irrelevant.