A question about DbC

[bearophile]

This is a simple D2 class that uses Contracts:


import std.c.stdio: printf;

class Car {
    int speed = 0;

    invariant() {
        printf("Car invariant: %d\n", speed);
        assert(speed >= 0);
    }

    this() {
        printf("Car constructor: %d\n", speed);
        speed = 0;
    }

    void setSpeed(int kmph)
        in {
            printf("Car.setSpeed precondition: %d\n", kmph);
            assert(kmph >= 0);
        } out {
            printf("Car.setSpeed postcondition: %d\n", speed);
            assert(speed == kmph);
        } body {
            printf("Car.setSpeed body\n");
            speed = kmph;
        }
}

void main() {
    auto c = new Car();
    c.setSpeed(10);
}


This is the output of the program, dmd 2.049:

Car constructor: 0
Car invariant: 0
Car.setSpeed precondition: 10
Car invariant: 0
Car.setSpeed body
Car invariant: 10
Car.setSpeed postcondition: 10

Is it correct? I think the invariant needs to run before the precondition and after the postcondition.

Bye,
bearophile