Invariants for methods

[Jens Mueller]

Andrei Alexandrescu wrote:
> 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.

Yes. I read the part about about inheritance and constructors and when I
tried my simple fix I struggled when I read about the inheritance part.
Because it does not fit in there properly.

> What I suggest you do is:
> 
> void move(...) {
>     debug {
>         const currentWidth = width;
>         const currentHeight = height;
>         scope (exit) {
>             assert(currentWidth == width);
>             assert(currentHeight == height);
>         }
>     }
>     ... body ...
> }

I like it.
Thanks.
What I'd even like better (because contracts are release specific):
release {
    const currentWidth = width;
    const currentHeight = height;
    scope (exit) {
        assert(currentWidth == width);
        assert(currentHeight == height);
    }
}
But that does not work. Why do we have special syntax for debug but not for
release. Both seem to me very similar. In the end I tend to think
release/debug as a shorthand for version(release/debug). But that's not
quite right. Somehow it's allowed to write version(unittest) {}
equivalently for unittest {}. But for debug/release there is no such
thing. Why this asymmetry?

Jens