View mode: basic / threaded / horizontal-split · Log in · Help
October 09, 2010
A question about DbC
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
October 09, 2010
Re: A question about DbC
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
October 09, 2010
Re: A question about DbC
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.
October 09, 2010
Re: A question about DbC
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
October 09, 2010
Re: A question about DbC
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.
October 09, 2010
Re: A question about DbC
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
October 09, 2010
Re: A question about DbC
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?
October 09, 2010
Re: A question about DbC
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
October 09, 2010
Re: A question about DbC
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.
October 09, 2010
Re: A question about DbC
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
« First   ‹ Prev
1 2 3
Top | Discussion index | About this forum | D home