Lutger wrote:
Between sharing the whole object and sharing scope lies specifying exactly
what to share, I'd think.
Here is one possible syntax, like regular function calls. Parameter types
can possibly be inferred and omitted:
void push(T value);
in {
out(length());
}
out(size_t oldLength) {
assert(value == top());
assert(length == oldLength + 1);
}
I like this, but I wouldnt make a regular function call:
void push(T value)
in {
out auto oldLength = length();
}
out {
assert(value == top());
assert(length() == oldLength + 1);
}
body {
...
}
If you declare variables as 'out' in a precondition, they are hidden
from the body and visible in the post condition.
The implementation of this is as easy as pushing oldLength on the stack
in the precondition and poping it in the postcondition.
Jeremie
