Invariants for methods

[bearophile]

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