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); }