Invariant and pre/post-conditions order

[Mail Mantis]

2012/1/20 bearophile <bearophileHUGS at lycos.com>:
> Walter has recently closed a bug report without fixing it and without an answer, it's about contract based programming:
> http://d.puremagic.com/issues/show_bug.cgi?id=5024
>
> So I'm asking for more info here.
>
> As reference I use this little program (I have improved it a bit compared to the one inside issue 5024):
>
>
>
> import std.c.stdio: printf;
>
> class Foo {
>    int x = 0;
>
>    invariant() {
>        printf("Foo invariant: x=%d\n", x);
>        assert(x >= 0);
>    }
>
>    this() {
>        printf("Foo constructor: x=%d\n", x);
>        x = 1;
>    }
>
>    void setX(int newx)
>        in {
>            printf("Foo.setX precondition: newx=%d\n", newx);
>            assert(newx >= 0);
>        } out {
>            printf("Foo.setX postcondition: x=%d\n", x);
>            assert(x == newx);
>        } body {
>            printf("Foo.setX body\n");
>            x = newx;
>        }
> }
>
> void main() {
>    auto c = new Foo();
>    c.setX(10);
> }
>
>
>
> Currently it prints this, that I don't like:
>
>
> Foo constructor: x=0
> Foo invariant: x=1
> Foo.setX precondition: newx=10
> Foo invariant: x=1
> Foo.setX body
> Foo invariant: x=10
> Foo.setX postcondition: x=10
>
>
>
> I'd like this order:
>
> Foo constructor: x=0
> Foo invariant: x=1
> Foo invariant: x=1
> Foo.setX precondition: newx=10
> Foo.setX body
> Foo.setX postcondition: x=10
> Foo invariant: x=10
>
>
> An example of why I think that's better. This is the same program with a bug:
>
>
> import std.c.stdio: printf;
>
> class Foo {
>    int x = 0;
>
>    invariant() {
>        printf("Foo invariant: x=%d\n", x);
>        assert(x >= 0); // line 8
>    }
>
>    this() {
>        printf("Foo constructor: x=%d\n", x);
>        x = 1;
>    }
>
>    void setX(int newx)
>        in {
>            printf("Foo.setX precondition: newx=%d\n", newx);
>            assert(newx >= 0);
>        } out {
>            printf("Foo.setX postcondition: x=%d\n", x);
>            assert(x == newx); // line 22
>        } body {
>            printf("Foo.setX body\n");
>            x = -newx;
>        }
> }
>
> void main() {
>    auto c = new Foo();
>    c.setX(10);
> }
>
>
> If I run it it gives:
> core.exception.AssertError at test2(8): Assertion failure
>
>
> So the bug is caught by a the generic invariant at line 8 instead of what I think is the correct place, the setX post-condition at line 22. The post-condition is a test meant to verify that the setX() body is correct, while the invariant contains more general tests. So I think it's more right to run the specific tests first, and the more general later.
>
> If I am mistaken please I'd like to know why the current design is better (or maybe why it's just equally good).
> Thank you :-)
> Bye,
> bearophile

I can think of somewhat this example:

struct Foo {
    int x = 1;

    invariant() {
        assert( x >= 0 );
    }

    int do_calc( int y )
    in {
        assert( y >= 0 );
    } out( result ) {
        assert( result >= 0 );
    } body {
        x *= -1;     //<- bug
        return x * y;
    }
}

The bug here is caused by accidental object corruption, and invariant
tells that. If assertions are swapped, we will get error at out
contract, which suggests that error is in calculus algorithm.