Communicating between in and out contracts

[Andrei Alexandrescu]

Consider a Stack interface:

interface Stack(T) {
    bool empty();
    ref T top();
    void push(T value);
    void pop();
    size_t length();
}

Let's attach contracts to the interface:

interface Stack(T) {
    bool empty();
    ref T top()
    in {
       assert(!empty());
    }
    void push(T value);
    out {
       assert(value == top());
    }
    void pop()
    in {
       assert(!empty());
    }
    size_t length()
    out(result) {
       assert((result == 0) == empty());
    }
}

So far so good. The problem is now that it's impossible to express the
contract "the length after push() is the length before plus 1."

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.

I was thinking of having the two contracts share the same scope. In that
case we can write:

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

Walter tried to implement that but it turned out to be very difficult
implementation-wise. We tossed around a couple of other ideas, without
making much progress. In particular inlining the contract bodies looks
more attractive than it really is. If you have any suggestion, please share.


Thanks,

Andrei