On 11/18/10 9:48 AM, Jens Mueller wrote:
I think of an member function invariant as something more fine-grained
than a class invariant. Of course calling move() needs to preserve the
class invariant but actually in case of move() it should also do
something more, namely before calling and after the call the width and
height should be the same. That's an invariant for the computation of
move(). How do I express it such that it will be compiled away when
disabling contracts (i.e. in release mode)?
There is a limitation of the current system in that the out contract
can't see the scope of the in contract. Walter and I tried to find a
solution, but it was technically difficult in the presence of inheritance.
What I suggest you do is:
void move(...) {
debug {
const currentWidth = width;
const currentHeight = height;
scope (exit) {
assert(currentWidth == width);
assert(currentHeight == height);
}
}
... body ...
}
Andrei
