Re: A question about DbC

[Denis Koroskin]

On Sat, 09 Oct 2010 07:16:10 +0400, bearophile <bearophileh...@lycos.com>  
wrote:

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

Given that pre-, post-conditions and invariants are all pure, it doesn't  
really matter in what order they are executed.