A question about DbC

[Denis Koroskin]

On Sat, 09 Oct 2010 07:16:10 +0400, bearophile <bearophileHUGS at 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.