Communicating between in and out contracts

Chris Nicholson-Sauls ibisbasenji at gmail.com
Wed Oct 14 13:39:35 PDT 2009


Andrei Alexandrescu wrote:
> 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

How hard would it be to do something like this: collect any local variables declared in 
the precondition into a structure, and make that structure transparently available to the 
postcondition.  So your push case above gets rewritten to something like this:

     __magic_tmp = {
         typeof( length() ) oldLength;
     }
     in {
         __magic_tmp.oldLength = length();
     }
     out {
         assert(value == top());
         assert(length == __magic_tmp.oldLength + 1);
     }

Honestly Lutger's idea of passing the data like parameters might be better, I'm just 
somehow uneasy about the look of "out(foo,bar)".

-- Chris Nicholson-Sauls



More information about the Digitalmars-d mailing list