Invariants for methods

[Jens Mueller]

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