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
