Out contracts: how to refer to objects' start state

[Idan Arye]

On Sunday, 26 May 2013 at 01:47:39 UTC, Andrei Alexandrescu wrote:
> On 5/25/13 9:18 PM, Adam D. Ruppe wrote:
>> On Sunday, 26 May 2013 at 01:12:35 UTC, Andrei Alexandrescu 
>> wrote:
>>> On 5/25/13 9:03 PM, Andrej Mitrovic wrote:
>>>> On 5/26/13, Andrei 
>>>> Alexandrescu<SeeWebsiteForEmail at erdani.org>
>>>>> in { auto oldLen = this.length; }
>>>> out { assert(this.length == in.oldLen + 1); }
>>
>>> Since every in.xyz expression could access an arbitrary 
>>> method of the
>>> old object,
>>
>> Here, in.oldLen refers to the local variable you defined in 
>> the in{}
>> scope, as opposed to plain oldLen which would be searing the 
>> out{} scope.
>
> Ohh, I see. Yes, that could work.
>
>
> Thanks,
>
> Andrei

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 { ... }
     }