Out contracts: how to refer to objects' start state

[Andrei Alexandrescu]

On 5/27/13 3:21 AM, Idan Arye wrote:
> Wouldn't it be simpler to define in the `in` clause what to pass to the
> out clause? Something like:
>
> class A {
> void fun()
> in { out oldLen = this.length; }
> out { assert(this.length == oldLen + 1); }
> body { ... }
> }
>
> Or even combine the two:
>
> class A {
> void fun()
> in { out oldLen = this.length; }
> out { assert(this.length == in.oldLen + 1); }
> body { ... }
> }

I think that got too cute.

Andrei