www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Invariants for methods

reply Jens Mueller <jens.k.mueller gmx.de> writes:
Hi,

I'm wondering what's a good way to do invariants for methods. In my
example I have a rectangle and one of its methods moves the upper left
of the rectangle. I have two invariants when moving a rectangle: The
width and the height do not change. I could do something like the
following:

void move(...) {
    int currentWidth = width;
    int currentHeight = height;
    // moving the rectangle here
    assert(currentWidth == width);
    assert(currentHeight == height);
}

I do not like it because it won't be completely compiled away in release
mode. The problem is that in the out contract I cannot access variables
of the in contract. If that was possible it just becomes:
in {
    int currentWidth = width;
    int currentHeight = height;
}
out {
    assert(currentWidth == width);
    assert(currentHeight == height);
}
body {
    // moving the rectangle here
}

Is there a solution that works right now? Are their plans to support
something like the above? Or should I do it differently?

Jens
Nov 18 2010
next sibling parent reply bearophile <bearophileHUGS lycos.com> writes:
Jens Mueller:

 I have a rectangle and one of its methods moves the upper left
 of the rectangle. I have two invariants when moving a rectangle: The
 width and the height do not change. I could do something like the
 following:
 
 void move(...) {
     int currentWidth = width;
     int currentHeight = height;
     // moving the rectangle here
     assert(currentWidth == width);
     assert(currentHeight == height);
 }

Probably you need one basic feature of DesignByContract that is missing still in D2, the "old" that allows at the end of a method to know the originals. It was discussed two or more times: http://www.digitalmars.com/d/archives/digitalmars/D/why_no_old_operator_in_function_postconditions_as_in_Eiffel_54654.html http://www.digitalmars.com/d/archives/digitalmars/D/Communicating_between_in_and_out_contracts_98252.html Once the feature is implemented you may solve your problem like this (minus syntax changes, but other solutions are possible): void move(...) in { // ... } out { assert(width == old.width); assert(height == old.height); } body { // moving the rectangle here } The problem of implementing the old was solved in C#4, it is named PrestateValues(OldValue), see page 8 here: http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf So probably this problem may be solved in D2 too. To solve this problem currently you may need to use ghost fields in your struct/class that memorize the older values... ghost fields wrapped in version(unittest) {...} or some version(debug). This is a bad solution. Bye, bearophile
Nov 18 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
Jens Mueller:

 I don't like the "old" approach.

Why? (It's the canonical way to solve the problem you have had. It is present in Eiffel and C# and probably something similar is present in the DbC for Java. But surely other solutions are possible.)
 Don't get your point here. You neither like the ghost fields (old) nor
 the debug {} approach as Andrei suggested?

I have written that answer of mine before reading Andrei answer.
 I mean after all the problem
 is not that important that one should bother too much.

The problem is important enough. In DbC it's very useful to have a safe&notbugprone way to test if a method has changed the precedent state correctly. Bye, bearophile
Nov 18 2010
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 11/18/10 1:57 PM, Jens Mueller wrote:
 bearophile wrote:
 Jens Mueller:

 I don't like the "old" approach.

Why? (It's the canonical way to solve the problem you have had. It is present in Eiffel and C# and probably something similar is present in the DbC for Java. But surely other solutions are possible.)

Somehow it doesn't feel right to me. It should just copy what is needed. Let's say I have some very big object. Now old is a copy before the execution of my member function. But I only check some little detail but I end of with having this big copy. I think the programmer knows what she's doing and she should have control about it. This copying behind the scenes seems surprising to me. Maybe I do not fully understand the approach.

The technique could be achieved by making "old" a keyword and copying only the fields accessed via "old". This approach was on the table. It has enough vagaries for me to dislike it. One approach that I very much prefer is that the "out" contract sees the scope of the "in" contract. That way, the user can define state in the "in" contract and then check it in the "out" contract. The approach is more general and easier to understand than the one based on the "old" object. Andrei
Nov 18 2010
parent bearophile <bearophileHUGS lycos.com> writes:
Jens Mueller:

 I see. bearophile even has a bug for this problem
 (http://d.puremagic.com/issues/show_bug.cgi?id=5027)

Issue 5027 is about ghost fields, not about "old", it's a related but separated problem/solution. In the meantime the idea of ghost fields was shot down for not being so important, so probably I will eventually close bug 5027...
 In particular I'm not sure whether bearophile agrees with having the out
 contract seeing the in contract's scope.

I write lot of posts, but I am not much expert yet, so I don't know what the better solution is. Both solutions have upsides and downsides: The upsides of the "old" solution is that it's simple looking for the user and it's known to other people that already know DbC from C# and Eiffel. But in the "old" the compiler has to find a way to automatically copy a class instance, this is something that all D has avoided. So in the end the "old" approach may be doomed in D. Seeing the precondition scope in the postcondition seems a good enough solution, it doesn't require new keywords, it does't ask the compiler to have an automatic way to copy class instances. The disadvantage is that it asks the programmer to invent ways to copy class instances every time the programmer wants to use a prestate, this is a lot of work, so I think very often class instances prestate will be not used (values prestate or pointer to values prestate will be used)... Even As another possible downside this solution may lead to DbC code less easy to reason about by automatic proof systems (this is a D DbC risk that I have discussed about some time ago, and it was dismissed) (Example: if you want a 2D matrix prestate you have to copy it in a foreach loop, this makes automatic analysis more and more difficult).
 But if that's a valid solution
 maybe he can add it to his bug report.

If you want to put it in bugzilla it's better to create something specific about DbC prestate, not about ghost fields. Bye, bearophile
Nov 18 2010
prev sibling parent bearophile <bearophileHUGS lycos.com> writes:
Jens Mueller:

This copying behind the scenes seems surprising to me. Maybe I do not fully
understand the

The compiler statically knows what things are needed in their older state (only ones accessed with "old." in the postcondition), so useless copying is avoided.
that right now there are more important problems.<

There are always more important problems. The most important one is probably that DMD development process doesn't taste Open Source enough yet (but the situation is improving: Phobos is slowly becoming more and more like an Open Source project, despite being not there yet).
I mean I do not know when people started complaining about Java missing proper
DbC but I'll guess it was a lot later.<

This is probably right.
If it starts itching then scratch it.<

I see, you like "just in time design", D is usually designed like that :-) I guess your problem was one of the best itches you will see on this.
I hope there is no inherent design problem.<

This time I think there is no inherent design problem, it's just a missing feature that may be added later.
I think this problem does not prevent D's success. I might be wrong here but
nobody is not switching to D because this does not work.<

Who knows, maybe a Eiffel programmer will refuse to use D because this feature is missing :-)
It's more the bugs/API changes/tools that keep people away. At least that's my
impression. It does not seem mature enough for some people.<

But I'd like a good language to build on. In the end Walter, Andrei and Don know way better than me. Bye, bearophile
Nov 18 2010
prev sibling next sibling parent Jens Mueller <jens.k.mueller gmx.de> writes:
bearophile wrote:
 Jens Mueller:
 
 I have a rectangle and one of its methods moves the upper left
 of the rectangle. I have two invariants when moving a rectangle: The
 width and the height do not change. I could do something like the
 following:
 
 void move(...) {
     int currentWidth = width;
     int currentHeight = height;
     // moving the rectangle here
     assert(currentWidth == width);
     assert(currentHeight == height);
 }

Probably you need one basic feature of DesignByContract that is missing still in D2, the "old" that allows at the end of a method to know the originals. It was discussed two or more times: http://www.digitalmars.com/d/archives/digitalmars/D/why_no_old_operator_in_function_postconditions_as_in_Eiffel_54654.html http://www.digitalmars.com/d/archives/digitalmars/D/Communicating_between_in_and_out_contracts_98252.html Once the feature is implemented you may solve your problem like this (minus syntax changes, but other solutions are possible):

Oh. I should have done better research. I don't like the "old" approach.
 void move(...)
     in {
         // ...
     } out {
         assert(width == old.width);
         assert(height == old.height);
     } body {
         // moving the rectangle here
     }
 
 
 The problem of implementing the old was solved in C#4, it is named
PrestateValues(OldValue), see page 8 here:
 http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf
 So probably this problem may be solved in D2 too.
 
 To solve this problem currently you may need to use ghost fields in your
struct/class that memorize the older values... ghost fields wrapped in
version(unittest) {...} or some version(debug). This is a bad solution.

Don't get your point here. You neither like the ghost fields (old) nor the debug {} approach as Andrei suggested? I mean after all the problem is not that important that one should bother too much. Maybe I'm too pragmatic. I'll try using it and see how it feels. Jens
Nov 18 2010
prev sibling next sibling parent Jens Mueller <jens.k.mueller gmx.de> writes:
bearophile wrote:
 Jens Mueller:
 
 I don't like the "old" approach.

Why? (It's the canonical way to solve the problem you have had. It is present in Eiffel and C# and probably something similar is present in the DbC for Java. But surely other solutions are possible.)

Somehow it doesn't feel right to me. It should just copy what is needed. Let's say I have some very big object. Now old is a copy before the execution of my member function. But I only check some little detail but I end of with having this big copy. I think the programmer knows what she's doing and she should have control about it. This copying behind the scenes seems surprising to me. Maybe I do not fully understand the approach.
 Don't get your point here. You neither like the ghost fields (old) nor
 the debug {} approach as Andrei suggested?

I have written that answer of mine before reading Andrei answer.

I see.
 I mean after all the problem
 is not that important that one should bother too much.

The problem is important enough. In DbC it's very useful to have a safe&notbugprone way to test if a method has changed the precedent state correctly.

I've seen the Java's Request for Enhancements you mentioned. DbC is number one. You're right one should do this properly but it seems to me that right now there are more important problems. I mean I do not know when people started complaining about Java missing proper DbC but I'll guess it was a lot later. If it starts itching then scratch it. I hope there is no inherent design problem. I think this problem does not prevent D's success. I might be wrong here but nobody is not switching to D because this does not work. It's more the bugs/API changes/tools that keep people away. At least that's my impression. It does not seem mature enough for some people. Jens
Nov 18 2010
prev sibling parent Jens Mueller <jens.k.mueller gmx.de> writes:
Andrei Alexandrescu wrote:
 On 11/18/10 1:57 PM, Jens Mueller wrote:
bearophile wrote:
Jens Mueller:

I don't like the "old" approach.

Why? (It's the canonical way to solve the problem you have had. It is present in Eiffel and C# and probably something similar is present in the DbC for Java. But surely other solutions are possible.)

Somehow it doesn't feel right to me. It should just copy what is needed. Let's say I have some very big object. Now old is a copy before the execution of my member function. But I only check some little detail but I end of with having this big copy. I think the programmer knows what she's doing and she should have control about it. This copying behind the scenes seems surprising to me. Maybe I do not fully understand the approach.

The technique could be achieved by making "old" a keyword and copying only the fields accessed via "old". This approach was on the table. It has enough vagaries for me to dislike it. One approach that I very much prefer is that the "out" contract sees the scope of the "in" contract. That way, the user can define state in the "in" contract and then check it in the "out" contract. The approach is more general and easier to understand than the one based on the "old" object.

I see. bearophile even has a bug for this problem (http://d.puremagic.com/issues/show_bug.cgi?id=5027). Somehow that does not surprise me. But I like it. Even though there seems to be some disagreement on a proper solution (right?) I think for the moment it's enough to have this bug report. In particular I'm not sure whether bearophile agrees with having the out contract seeing the in contract's scope. But if that's a valid solution maybe he can add it to his bug report. Jens
Nov 18 2010