Invariants for methods

[Jens Mueller]

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