Communicating between in and out contracts

[Jeremie Pelletier]

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