Communicating between in and out contracts

[Lutger]

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