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

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

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

On Saturday 09 October 2010 03:09:30 Denis Koroskin wrote:
> Given that pre-, post-conditions and invariants are all pure, it doesn't really matter in what order they are executed.

In effect yes, but they aren't actually pure. If they were, you couldn't use stuff like writeln() in them. However, since they go away in release builds and aren't supposed to have any effect on the program (beyond throwing AssertErrors on failed assertions), they are in effect pure, so you're essentially correct. But still, they aren't actually pure.

- Jonathan M Davis

On Sat, 09 Oct 2010 14:20:18 +0400, Jonathan M Davis <jmdavisProg@gmx.com> wrote:

> On Saturday 09 October 2010 03:09:30 Denis Koroskin wrote:
>> Given that pre-, post-conditions and invariants are all pure, it doesn't
>> really matter in what order they are executed.
>
> In effect yes, but they aren't actually pure. If they were, you couldn't use stuff
> like writeln() in them. However, since they go away in release builds and aren't
> supposed to have any effect on the program (beyond throwing AssertErrors on
> failed assertions), they are in effect pure, so you're essentially correct. But
> still, they aren't actually pure.
>
> - Jonathan M Davis

Well, I meant they are conceptually pure.
But do believe you shouldn't be able to use writeln in code like that. Why would you do it anyway? It's more or less like using assert just for a console output:

try {
    assert(false, "message");
} catch {
}

Put your logging stuff into the body, not into the contracts.

On Saturday 09 October 2010 03:25:48 Denis Koroskin wrote:
> Well, I meant they are conceptually pure.

Yes, they are conceptually pure, just not actually pure.

> But do believe you shouldn't be able to use writeln in code like that. Why would you do it anyway? It's more or less like using assert just for a console output:
> 
> try {
>      assert(false, "message");
> } catch {
> }
> 
> Put your logging stuff into the body, not into the contracts.

It's for debugging, not logging. It's highly useful for stuff like figuring out which a contract is failing. That's the main reason why contracts are only conceptually pure rather than actually pure.

- Jonathan M Davis

On Sat, 09 Oct 2010 14:44:41 +0400, Jonathan M Davis <jmdavisProg@gmx.com> wrote:

> On Saturday 09 October 2010 03:25:48 Denis Koroskin wrote:
>> Well, I meant they are conceptually pure.
>
> Yes, they are conceptually pure, just not actually pure.
>
>> But do believe you shouldn't be able to use writeln in code like that. Why
>> would you do it anyway? It's more or less like using assert just for a
>> console output:
>>
>> try {
>>      assert(false, "message");
>> } catch {
>> }
>>
>> Put your logging stuff into the body, not into the contracts.
>
> It's for debugging, not logging. It's highly useful for stuff like figuring out
> which a contract is failing. That's the main reason why contracts are only
> conceptually pure rather than actually pure.
>
> - Jonathan M Davis

Why not just throw an exception and get a nice stack trace?

On Saturday 09 October 2010 03:47:52 Denis Koroskin wrote:
> Why not just throw an exception and get a nice stack trace?

You get a stack trace anyway with an assertion failure. And sure, they _could_ make it so that the only way to output anything from a contract is to use an exception, but not only would that be more of a pain than using writeln(), but it would mean that the only time you could output anything would be on failure. As it is, you can print something every time that a contract is run. You couldn't do that with an exception.

- Jonathan M Davis

On Sat, 09 Oct 2010 15:06:40 +0400, Jonathan M Davis <jmdavisProg@gmx.com> wrote:

> On Saturday 09 October 2010 03:47:52 Denis Koroskin wrote:
>> Why not just throw an exception and get a nice stack trace?
>
> You get a stack trace anyway with an assertion failure. And sure, they _could_
> make it so that the only way to output anything from a contract is to use an
> exception, but not only would that be more of a pain than using writeln(), but
> it would mean that the only time you could output anything would be on failure.
> As it is, you can print something every time that a contract is run. You
> couldn't do that with an exception.
>
> - Jonathan M Davis

I could do the same within a function body.

Anyway, I don't see the discussion going anywhere, it's just a matter of preference and I don't really mind yours.

On Saturday 09 October 2010 04:23:25 Denis Koroskin wrote:
> On Sat, 09 Oct 2010 15:06:40 +0400, Jonathan M Davis <jmdavisProg@gmx.com>
> 
> wrote:
> > On Saturday 09 October 2010 03:47:52 Denis Koroskin wrote:
> >> Why not just throw an exception and get a nice stack trace?
> > 
> > You get a stack trace anyway with an assertion failure. And sure, they
> > _could_
> > make it so that the only way to output anything from a contract is to
> > use an
> > exception, but not only would that be more of a pain than using
> > writeln(), but
> > it would mean that the only time you could output anything would be on
> > failure.
> > As it is, you can print something every time that a contract is run. You
> > couldn't do that with an exception.
> > 
> > - Jonathan M Davis
> 
> I could do the same within a function body.
> 
> Anyway, I don't see the discussion going anywhere, it's just a matter of preference and I don't really mind yours.

Well, regardless of what we think and what the pros and cons of the situation actually are, as I understand it, the whole reason that contracts aren't pure is so that you can use writeln() in them for debugging.

- Jonathan M Davis