Invariant and pre/post-conditions order

[bearophile]

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