For some class methods, to express comprehensive out{} contracts it is necessary to be able to refer to the state of the class object before the operation as well as after it e.g. if the method adds something to a container you need to be able to specify that nothing was accidentally deleted from the container during the method.  I've scoured the language specification and Andrei's book for advice on how to do this without any luck.

Can it be done and, if so, how?

Thanks
Peter

On 5/25/13 8:38 PM, Peter Williams wrote:
> For some class methods, to express comprehensive out{} contracts it is
> necessary to be able to refer to the state of the class object before
> the operation as well as after it e.g. if the method adds something to a
> container you need to be able to specify that nothing was accidentally
> deleted from the container during the method. I've scoured the language
> specification and Andrei's book for advice on how to do this without any
> luck.
>
> Can it be done and, if so, how?
>
> Thanks
> Peter

Unfortunately we don't have a solution to that. A while ago I proposed that the "in" and "out" contracts share the same scope. That would allow us to do:

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.


Andrei

On 5/26/13, Andrei Alexandrescu <SeeWebsiteForEmail@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.

On 5/25/13 9:03 PM, Andrej Mitrovic wrote:
> On 5/26/13, Andrei Alexandrescu<SeeWebsiteForEmail@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

Andrei Alexandrescu:

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

The "prestate" is an important part of contract programming. So it's better to look for some other solution to implement it.

---------------

Andrej Mitrovic:

> "in" is a keyword so it shouldn't break any existing code.

Usually languages use the word "old" instead of "in" for this purpose. But I think "in" is acceptable. And it's much better than not having the prestate.

Bye,
bearophile

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@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.

Andrei Alexandrescu:

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

Then we have to take a look at how C# and Ada solve such problem (both support the pre-state).

Bye,
bearophile

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@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

On 26/05/13 10:43, Andrei Alexandrescu wrote:
> On 5/25/13 8:38 PM, Peter Williams wrote:
>> For some class methods, to express comprehensive out{} contracts it is
>> necessary to be able to refer to the state of the class object before
>> the operation as well as after it e.g. if the method adds something to a
>> container you need to be able to specify that nothing was accidentally
>> deleted from the container during the method. I've scoured the language
>> specification and Andrei's book for advice on how to do this without any
>> luck.
>>
>> Can it be done and, if so, how?
>>
>> Thanks
>> Peter
>
> Unfortunately we don't have a solution to that. A while ago I proposed
> that the "in" and "out" contracts share the same scope. That would allow
> us to do:
>
> 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.

That looks like a good solution to me.

> Today it would break too much code to introduce even if feasible.

How would it break code?  I've tried to imagine how but have failed.

Peter

On 26/05/13 11:47, 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@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.

That revelation also answers my question about how it could break code.

Peter