Invariants for methods

[Jonathan M Davis]

On Thursday 18 November 2010 12:08:19 Jens Mueller wrote:
> 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?

One thing that you need to realize is that the -release and -debug flags are 
_completely_ unrelated. You can use none, or one, or even both.

-release disables assertions (other than assert(0)) - including removing all 
pre-conditions, post-condition, and invariants - and removes array bounds 
checking for @system and @trusted functions.

-debug enables all debug blocks.

So, you can have

* Neither flag: All assertions, contracts, and array bounds checking are enabled, 
and debug blocks are not compiled in.

* -release only: All assertions, contracts, and array bounds checking for 
@system and @trusted functions are removed. debug blocks are not compiled in.

* -debug only: All assertions, contracts, and array bounds checking are enabled, 
and debug blocks are compiled in.

* Both flags: All assertions, contracts, and array bounds checking in @system and 
@trusted functions are removed. debug blocks are compiled in.


So, the flags in question are quite confusing really, and talking about debug 
mode doesn't actually make sense when you think about it. You have release mode 
and non-release mode. And you either have debug blocks enabled or you don't. And 
on top of that, you have whether debug symbols are enabled or not (even worse, 
there are two different flags for enabling debug symobls: -g and -gc). So, the 
flags as they are make the whole release vs debug build thing really confusing, 
and they're probably not terms that really should be used unless you're talking 
about your specific build process and the specific set of flags that you use for 
building for release builds and the specific set of flags that you use for debug 
builds. But talking about release and debug builds is so ingrained in people, 
that they keep using the terms anyway, and most people probably don't quite 
understand the imprecision of the terms with regards to dmd.

- Jonathan M Davis