Out contracts: how to refer to objects' start state

[Andrei Alexandrescu]

On 5/25/13 9:03 PM, Andrej Mitrovic wrote:
> On 5/26/13, Andrei Alexandrescu<SeeWebsiteForEmail at erdani.org>  wrote:
>> class A {
>>     void fun()
>>     in { auto oldLen = this.length; }
>>     out { assert(this.length == oldLen + 1); }
>>     body { ... }
>> }
>>
>> That was technically difficult to do back then, and fell by the wayside.
>> Today it would break too much code to introduce even if feasible.
>
> Perhaps we could support this by allowing qualification of the in block:
>
> out { assert(this.length == in.oldLen + 1); }
>
> "in" is a keyword so it shouldn't break any existing code.

The problem with this is well-defining it. Since every in.xyz expression 
could access an arbitrary method of the old object, that means the whole 
object would need to be somehow duplicated. Alternatively, all in.xyz 
expressions would need to be evaluated before the function's entry 
point, which is weird (what order? how about side effects? etc).

The whole in.xyz trick (or as in Eiffel old.xyz) is inherently flimsy. 
I'd rather allow the user to save and check their own state instead, 
without resorting to a complicated definition.


Andrei