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
    }



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

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

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
parent reply 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

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

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

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

"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


approach.<

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 parent reply bearophile <bearophileHUGS lycos.com> writes:
Andrei:


I don't think they have contracts in interfaces, which is where most difficulty
lies.<


There is some discussion about this topic at page 11 here:
http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf



At any rate, it's not that we can't do it, it was just a large effort that we
decided to postpone.<


Postponing its solution (to D3, if needed) is good.



Is there anything wrong with the workaround I suggested?<


We have had a discussion like this many times, about unittests, ranged
integers, nonull references, etc, so probably we think about languages in
different ways.

Your workaround is an intelligent trick, I was not able to invent it, and it's
a solution better than the one I have used to solve it (ghost fields in
debug{}).

In my opinion in a language you must not need to use intelligent tricks to
solve basic problems (and referring to the old state is one of the important
parts of DbC).

Bye,
bearophile
Nov 18 2010
next sibling parent reply Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 11/18/10 1:07 PM, bearophile wrote:

 Andrei:


 I don't think they have contracts in interfaces, which is where most
difficulty lies.<


 There is some discussion about this topic at page 11 here:
 http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf



 At any rate, it's not that we can't do it, it was just a large effort that we
decided to postpone.<


 Postponing its solution (to D3, if needed) is good.



 Is there anything wrong with the workaround I suggested?<


 We have had a discussion like this many times, about unittests, ranged
integers, nonull references, etc, so probably we think about languages in
different ways.

 Your workaround is an intelligent trick, I was not able to invent it, and it's
a solution better than the one I have used to solve it (ghost fields in
debug{}).

 In my opinion in a language you must not need to use intelligent tricks to
solve basic problems (and referring to the old state is one of the important
parts of DbC).

 Bye,
 bearophile


I don't see anything remotely clever in the solution I suggested. At 
some point it's worth starting to use the language to devise solutions 
to problems instead of inventing a new feature for any problem that 
comes about.

Andrei
Nov 18 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
Andrei:


 I don't see anything remotely clever in the solution I suggested.


I am not clever enough...



 At some point it's worth starting to use the language to devise solutions 
 to problems instead of inventing a new feature for any problem that 
 comes about.


That was not a new unexpected problem, it was an example of missing brick of
the D DbC. It's like you remove preconditions: then something is missing in the
frame. Loop invariants and loop variants are minor feature of DbC and they
probably may be spared in D (and when necessary loop invariants may be
implemented manually with a call to a pure function), but prestate access is
something I/you need often when you want to use DbC, it's not there in Eiffel


Your view of how to design a language is probably different from mine.

Bye,
bearophile
Nov 18 2010
parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 11/18/10 2:02 PM, bearophile wrote:

 Andrei:


 I don't see anything remotely clever in the solution I suggested.


 I am not clever enough...


This would be more credible if this were indeed a matter of being 
clever. It is a basic juxtaposition of ubiquitous features.


 At some point it's worth starting to use the language to devise solutions
 to problems instead of inventing a new feature for any problem that
 comes about.


 That was not a new unexpected problem, it was an example of missing


brick of the D DbC. It's like you remove preconditions: then something
is missing in the frame. Loop invariants and loop variants are minor
feature of DbC and they probably may be spared in D (and when necessary
loop invariants may be implemented manually with a call to a pure
function), but prestate access is something I/you need often when you


 Your view of how to design a language is probably different from mine.


I allowed myself to reflect a bit on the "moving average", so to say, of 
your posts, than on this particular one. That moving average reveals a 
trigger happiness about adding features instead of using existing 
features. It also reveals a consistent effort to find what other 
languages do better than D, which is good. What is missing, however, is 
taking advantage of the many things that D _does_ do well (and better 
than various other languages).

It's not impossible our views on language design differ, but that's 
nothing odd as the process and appreciating the results are highly 
subjective.


Andrei
Nov 18 2010
prev sibling parent Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:
On 11/18/10 1:07 PM, bearophile wrote:

 Andrei:


 I don't think they have contracts in interfaces, which is where most
difficulty lies.<


 There is some discussion about this topic at page 11 here:
 http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf


That approach is essentially a workaround for a problem that I consider 
crucial (interfaces must be able to specify contracts) that D solves 
properly.

Andrei
Nov 18 2010