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 think this could work. One of Walter's ideas was to pass the entire old object as an argument to out. Passing handpicked data is more work for the user but faster.

Perhaps this would simplify things a bit:

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

Whatever parameters you pass to out they'd be matched by name with stuff defined in the "in" contract. That poses a problem because until now out(whatever) automatically passed the result to the out contract under the name "whatever".


Andrei

Reply via email to