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
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 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
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
next sibling parent reply "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; }


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


 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
May 25 2013
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; }


 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
May 25 2013
prev sibling parent reply "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; }


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



(both support the pre-state).

Bye,
bearophile
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 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 parent reply "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
next sibling parent reply 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
next sibling parent reply "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
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
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 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