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