www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.learn - A question about DbC

reply bearophile <bearophileHUGS lycos.com> writes:
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
Oct 08 2010
next sibling parent reply Jonathan M Davis <jmdavisProg gmx.com> writes:
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
Oct 08 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
Jonathan M Davis:

 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.

They may contain different tests. Bye, bearophile
Oct 09 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
Jonathan M Davis:

 if the state couldn't have changed since the last public function call, the
running
 the invariant before the function call is pointless.

The post-condition of a method doesn't need to make sure the class is in a correct state, all it has to test is that its output (including the instance state it has modified) is correct. The invariant instead has to test that the whole class instance is in a meaningful state. So method post-condition and class invariant contain different code and they must be run both, because the post-condition has to test just the class instance state it has changed, and not that such changes are globally coherent with the whole class instance state. Bye, bearophile
Oct 09 2010
parent reply =?UTF-8?B?IkrDqXLDtG1lIE0uIEJlcmdlciI=?= <jeberger free.fr> writes:
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

bearophile wrote:
 Jonathan M Davis:
=20
 if the state couldn't have changed since the last public function call=


 the invariant before the function call is pointless.

The post-condition of a method doesn't need to make sure the class is i=

nstance state it has modified) is correct.
=20
 The invariant instead has to test that the whole class instance is in a=

ifferent code and they must be run both, because the post-condition has t= o test just the class instance state it has changed, and not that such ch= anges are globally coherent with the whole class instance state.
=20

invariant. It is about running the invariant twice: both before and after the function. This is completely independent from any pre- or post-conditions there may be. Jerome --=20 mailto:jeberger free.fr http://jeberger.free.fr Jabber: jeberger jabber.fr
Oct 09 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
J. Berger:

 	Jonathan's point is not about running the post-condition and the
 invariant. It is about running the invariant twice: both before and
 after the function. This is completely independent from any pre- or
 post-conditions there may be.

You are missing something still. C = a class with Dbc foo = nonstatic method of C fooargs = input arguments of foo r = result of foo S = state of the class instance foo fooS = a subset of S, the part of the state influenced by foo noFoo = S - fooS = part of S not influenced by foo Inv = C invariant, that tests for coherence of the whole S prefoo = pre-condition of foo postfoo = post-condition of foo Let's say DMD runs things in this order (this is not currently true but I think this is more correct): Inv prefoo foo postfoo Inv Then: - The first Inv tests that S is coherent - prefoo tests that fooargs are correct (and maybe even that fooS is correct) - postfoo tests that r and fooS are correct - Inv tests that S is coherent It's necessary to run Inv before and after foo because postfoo has not tested that the whole S is coherent. foo is able to modify just fooS, it can't touch noFoo, but you need to run Inv again because inside Inv it may be present a predicate1(fooS, noFoo) that is true according to the relation between fooS and noFoo. So even if noFoo is unchanged, changes to fooS may be enough to invalidate predicate1. Bye, bearophile
Oct 09 2010
parent reply =?UTF-8?B?IkrDqXLDtG1lIE0uIEJlcmdlciI=?= <jeberger free.fr> writes:
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

bearophile wrote:
 J. Berger:
=20
 	Jonathan's point is not about running the post-condition and the
 invariant. It is about running the invariant twice: both before and
 after the function. This is completely independent from any pre- or
 post-conditions there may be.

You are missing something still. =20

 ... example pseudo-code

This is more or less what Jonathan said in his last post. Jerome --=20 mailto:jeberger free.fr http://jeberger.free.fr Jabber: jeberger jabber.fr
Oct 09 2010
next sibling parent reply bearophile <bearophileHUGS lycos.com> writes:
J. Berger:

 This is more or less what Jonathan said in his last post.

You are right, if the state isn't changed between two method calls, there's no point in calling the invariant two times after the method call and before the next method call. Bye, bearophile
Oct 09 2010
parent bearophile <bearophileHUGS lycos.com> writes:
Jonathan M Davis:

 Yes, the problem creeps in because public methods are not necessarily the only 
 way to alter the state of an object. Running the invariant before the function 
 is run is actually a good catch on Walter's part. I wouldn't have thought of
it 
 precisely because it wouldn't be necessary if the only way to alter an object
is 
 through it's public methods (and that's often how classe/structs are written).

Partially unrelated: if a method is const, it doesn't change instance state, so there's no need to test the invariant after the method call... well unfortunately this is not true, because the invariant tests the static attributes too, that a const method may modify. Regarding the static state, in another implementation of DbC I have seen the "class static invariant" too, that tests the static class attributes, but I don't understand why it may be useful... Bye, bearophile
Oct 09 2010
prev sibling parent Jonathan M Davis <jmdavisProg gmx.com> writes:
On Saturday 09 October 2010 08:39:30 bearophile wrote:
 J. Berger:
 This is more or less what Jonathan said in his last post.

You are right, if the state isn't changed between two method calls, there's no point in calling the invariant two times after the method call and before the next method call.

Yes, the problem creeps in because public methods are not necessarily the only way to alter the state of an object. Running the invariant before the function is run is actually a good catch on Walter's part. I wouldn't have thought of it precisely because it wouldn't be necessary if the only way to alter an object is through it's public methods (and that's often how classe/structs are written). - Jonathan M Davis
Oct 09 2010
prev sibling next sibling parent reply "Denis Koroskin" <2korden gmail.com> writes:
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.
Oct 09 2010
next sibling parent Jonathan M Davis <jmdavisProg gmx.com> writes:
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
Oct 09 2010
prev sibling parent "Denis Koroskin" <2korden gmail.com> writes:
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.
Oct 09 2010
prev sibling next sibling parent Jonathan M Davis <jmdavisProg gmx.com> writes:
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
Oct 09 2010
prev sibling next sibling parent "Denis Koroskin" <2korden gmail.com> writes:
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?
Oct 09 2010
prev sibling next sibling parent reply Jonathan M Davis <jmdavisProg gmx.com> writes:
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
Oct 09 2010
parent bearophile <bearophileHUGS lycos.com> writes:
Denis Koroskin:

 Why do you think Walter disallowed throwing from  
 contracts (other than asserts) in first place?

Probably because exceptions have no place in contracts. If a contract fails, the program is buggy, and it needs to stop. Contracts need to contain logical expressions that need to true for the contract to pass. And the compiler has to enforce the contracts statically as much as possible. Thank you for all the answers. I'll add something in bugzilla soon. Bye, bearophile
Oct 09 2010
prev sibling next sibling parent "Denis Koroskin" <2korden gmail.com> writes:
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.
Oct 09 2010
prev sibling next sibling parent Jonathan M Davis <jmdavisProg gmx.com> writes:
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
Oct 09 2010
prev sibling next sibling parent "Denis Koroskin" <2korden gmail.com> writes:
On Sat, 09 Oct 2010 15:32:26 +0400, Jonathan M Davis <jmdavisProg gmx.com>  
wrote:

 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.

 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

I don't thinks so, it's rather the feature isn't fully implemented yet. For example, up until recently you couldn't throw Exceptions from contracts, and was only be able to use asserts. That got changed because it was an easy to violate rule (by calling some other function that throws, e.g. enforce). Why do you think Walter disallowed throwing from contracts (other than asserts) in first place?
Oct 09 2010
prev sibling next sibling parent Jonathan M Davis <jmdavisProg gmx.com> writes:
On Saturday 09 October 2010 04:49:08 Denis Koroskin wrote:
 On Sat, 09 Oct 2010 15:32:26 +0400, Jonathan M Davis <jmdavisProg gmx.com>
 
 wrote:
 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

I don't thinks so, it's rather the feature isn't fully implemented yet. For example, up until recently you couldn't throw Exceptions from contracts, and was only be able to use asserts. That got changed because it was an easy to violate rule (by calling some other function that throws, e.g. enforce). Why do you think Walter disallowed throwing from contracts (other than asserts) in first place?

IIRC, TDPL specifically says that the reason that contracts aren't pure is so that you can use writeln() for debugging. And as for exceptions, why _would_ you throw them from a contract? Contracts are supposed to contain assertions and whatever code is necessary to set up what's given to them. That's it. Exceptions are used for error handling, which contracts aren't supposed to do. - Jonathan M Davis
Oct 09 2010
prev sibling parent Jonathan M Davis <jmdavisProg gmx.com> writes:
On Saturday 09 October 2010 06:02:52 bearophile wrote:
 Jonathan M Davis:
 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.

They may contain different tests.

True, but assuming that there is no way to access the state of the object except through its public functions, then running the invariant before executing a public function is pointless, because it was already run after the last public function was called, and there's no way that the state of the object could have changed in the interim. However, given that returned references and pointers as well as public member variables would allow you to alter an object outside of its public functions, the object's state could have changed between its last public function call and the new public function call, so that's probably why the invariant is run before the public function is. However, if the state couldn't have changed since the last public function call, the running the invariant before the function call is pointless. - Jonathan M Davis
Oct 09 2010