Invariants for methods
Jens Mueller
jens.k.mueller at gmx.de
Thu Nov 18 12:08:19 PST 2010
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
More information about the Digitalmars-d
mailing list