Communicating between in and out contracts

[Rainer Deyke]

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'.  In other words, this functionality:

>    void push(T value);
>    in {
>       auto oldLength = length();
>    }
>    out {
>       assert(value == top());
>       assert(length == oldLength + 1);
>    }

...can be expressed with this syntax:

   void push(T value);
   out {
      assert(value == top());
      assert(length == old length + 1);
   }

The syntax with 'old' is more concise, easier to read, and does the same
thing.  What's wrong with it (other than adding yet another keyword to
the language)?


-- 
Rainer Deyke - rainerd at eldwood.com