Re: 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<seewebsiteforem...@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 { ... }
    }