www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Out contracts: how to refer to objects' start state

reply Peter Williams <pwil3058 bigpond.net.au> writes:
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
May 25 2013
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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
May 25 2013
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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
May 25 2013
parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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; }



 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
May 25 2013
parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
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
May 27 2013
prev sibling next sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 5/27/13 3:37 AM, deadalnix wrote:
 On Sunday, 26 May 2013 at 00:43:36 UTC, Andrei Alexandrescu wrote:
 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.

Can you expand more on the breakage risk please ?

Easy - name collisions between the in and the out blocks. Andrei
May 27 2013
prev sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 5/27/13 3:42 AM, Jonathan M Davis wrote:
 On Monday, May 27, 2013 09:37:38 deadalnix wrote:
 On Sunday, 26 May 2013 at 00:43:36 UTC, Andrei Alexandrescu wrote:
 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.

Can you expand more on the breakage risk please ?

If nothing else, it would mean that the variables inside of the in block would not go out of scope when the in block ended, so their destructors would not be called and the like, whereas now they would be. The same goes for scope statements in the in block. I don't know how much of an issue any of that is realistically though. But Andrei may have other reasons why it would be a problem.

Oh, destructors too. Andrei
May 27 2013
prev sibling next sibling parent Andrej Mitrovic <andrej.mitrovich gmail.com> writes:
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.
May 25 2013
prev sibling next sibling parent "bearophile" <bearophileHUGS lycos.com> writes:
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
May 25 2013
prev sibling next sibling parent "Adam D. Ruppe" <destructionator gmail.com> writes:
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; }



 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.
May 25 2013
prev sibling next sibling parent "bearophile" <bearophileHUGS lycos.com> writes:
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
May 25 2013
prev sibling next sibling parent Peter Williams <pwil3058 bigpond.net.au> writes:
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
May 25 2013
prev sibling next sibling parent Peter Williams <pwil3058 bigpond.net.au> writes:
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; }



 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
May 25 2013
prev sibling next sibling parent "Idan Arye" <GenericNPC gmail.com> writes:
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 erdani.org>
 in { auto oldLen = this.length; }



 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 { ... } }
May 27 2013
prev sibling next sibling parent "deadalnix" <deadalnix gmail.com> writes:
On Sunday, 26 May 2013 at 00:43:36 UTC, Andrei Alexandrescu wrote:
 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.

Can you expand more on the breakage risk please ?
May 27 2013
prev sibling next sibling parent Jonathan M Davis <jmdavisProg gmx.com> writes:
On Monday, May 27, 2013 09:37:38 deadalnix wrote:
 On Sunday, 26 May 2013 at 00:43:36 UTC, Andrei Alexandrescu wrote:
 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.

Can you expand more on the breakage risk please ?

If nothing else, it would mean that the variables inside of the in block would not go out of scope when the in block ended, so their destructors would not be called and the like, whereas now they would be. The same goes for scope statements in the in block. I don't know how much of an issue any of that is realistically though. But Andrei may have other reasons why it would be a problem. - Jonathan M Davis
May 27 2013
prev sibling next sibling parent "deadalnix" <deadalnix gmail.com> writes:
On Monday, 27 May 2013 at 07:42:44 UTC, Jonathan M Davis wrote:
 On Monday, May 27, 2013 09:37:38 deadalnix wrote:
 On Sunday, 26 May 2013 at 00:43:36 UTC, Andrei Alexandrescu 
 wrote:
 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.

Can you expand more on the breakage risk please ?

If nothing else, it would mean that the variables inside of the in block would not go out of scope when the in block ended, so their destructors would not be called and the like, whereas now they would be. The same goes for scope statements in the in block. I don't know how much of an issue any of that is realistically though. But Andrei may have other reasons why it would be a problem.

You are right, destructor is an issue. The risk of name collision exists as well but I don't think it is realistically that widespread in actual codebase.
May 27 2013
prev sibling parent "Idan Arye" <GenericNPC gmail.com> writes:
On Monday, 27 May 2013 at 09:06:58 UTC, deadalnix wrote:
 On Monday, 27 May 2013 at 07:42:44 UTC, Jonathan M Davis wrote:
 On Monday, May 27, 2013 09:37:38 deadalnix wrote:
 On Sunday, 26 May 2013 at 00:43:36 UTC, Andrei Alexandrescu 
 wrote:
 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.

Can you expand more on the breakage risk please ?

If nothing else, it would mean that the variables inside of the in block would not go out of scope when the in block ended, so their destructors would not be called and the like, whereas now they would be. The same goes for scope statements in the in block. I don't know how much of an issue any of that is realistically though. But Andrei may have other reasons why it would be a problem.

You are right, destructor is an issue. The risk of name collision exists as well but I don't think it is realistically that widespread in actual codebase.

Yet another reason why those variable should be declared as such in the `in` clause. Variables declared in the `in` clause using the `out` attribute would have their destruction done after the `out` clause, and all other variables declared in the `in` clause would be destructed after the `in` clause.
May 27 2013