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 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
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:
bearophile wrote:

 Jonathan M Davis:
=20

 if the state couldn't have changed since the last public function call=




, the running

 the invariant before the function call is pointless.


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


n a correct state, all it has to test is that its output (including the i=
nstance state it has modified) is correct.

=20
 The invariant instead has to test that the whole class instance is in a=


 meaningful state. So method post-condition and class invariant contain d=
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


	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.

		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:
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.


=20
 You are missing something still.
=20


	No.


 ... 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
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 reply 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
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 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
parent reply 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
parent reply "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
parent reply 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
parent reply "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
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 reply "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
parent reply 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
parent reply "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.  


 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?
Oct 09 2010
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 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