A question about DbC

[Jonathan M Davis]

On Friday 08 October 2010 20:16:10 bearophile 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.

Why? The invariant only really needs to be run after each public function runs. 
It could be before or after the postcondition. Both the postcondition and 
invariant need to be true and they're completely independent, so they could be 
run in either order. What's odder is that the invariant is run after the 
precondition. That shouldn't be necessary, since any changes to the object would 
have been verifed after the last time that a public member function was called. 
Maybe it's because of the possibility of member variables being altered because 
they were returned by reference or because of public member variables having 
possibly been altered. Regardless, since the postcondition and invariant are 
indepedent, it shouldn't matter which order they run in - particularly since 
they are essentially pure, even if purity is not enforced for them (that is, 
unless you're doing something stupid, neither of them will alter the state of 
the object, so they could be run in either order).

- Jonathan M Davis