Invariants for methods

[Andrei Alexandrescu]

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