www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Invariant and pre/post-conditions order

reply bearophile <bearophileHUGS lycos.com> writes:
Walter has recently closed a bug report without fixing it and without an
answer, it's about contract based programming:
http://d.puremagic.com/issues/show_bug.cgi?id=5024

So I'm asking for more info here.

As reference I use this little program (I have improved it a bit compared to
the one inside issue 5024):



import std.c.stdio: printf;

class Foo {
    int x = 0;

    invariant() {
        printf("Foo invariant: x=%d\n", x);
        assert(x >= 0);
    }

    this() {
        printf("Foo constructor: x=%d\n", x);
        x = 1;
    }

    void setX(int newx)
        in {
            printf("Foo.setX precondition: newx=%d\n", newx);
            assert(newx >= 0);
        } out {
            printf("Foo.setX postcondition: x=%d\n", x);
            assert(x == newx);
        } body {
            printf("Foo.setX body\n");
            x = newx;
        }
}

void main() {
    auto c = new Foo();
    c.setX(10);
}



Currently it prints this, that I don't like:


Foo constructor: x=0
Foo invariant: x=1
Foo.setX precondition: newx=10
Foo invariant: x=1
Foo.setX body
Foo invariant: x=10
Foo.setX postcondition: x=10



I'd like this order:

Foo constructor: x=0
Foo invariant: x=1
Foo invariant: x=1
Foo.setX precondition: newx=10
Foo.setX body
Foo.setX postcondition: x=10
Foo invariant: x=10


An example of why I think that's better. This is the same program with a bug:


import std.c.stdio: printf;

class Foo {
    int x = 0;

    invariant() {
        printf("Foo invariant: x=%d\n", x);
        assert(x >= 0); // line 8
    }

    this() {
        printf("Foo constructor: x=%d\n", x);
        x = 1;
    }

    void setX(int newx)
        in {
            printf("Foo.setX precondition: newx=%d\n", newx);
            assert(newx >= 0);
        } out {
            printf("Foo.setX postcondition: x=%d\n", x);
            assert(x == newx); // line 22
        } body {
            printf("Foo.setX body\n");
            x = -newx;
        }
}

void main() {
    auto c = new Foo();
    c.setX(10);
}


If I run it it gives:
core.exception.AssertError test2(8): Assertion failure


So the bug is caught by a the generic invariant at line 8 instead of what I
think is the correct place, the setX post-condition at line 22. The
post-condition is a test meant to verify that the setX() body is correct, while
the invariant contains more general tests. So I think it's more right to run
the specific tests first, and the more general later.

If I am mistaken please I'd like to know why the current design is better (or
maybe why it's just equally good).
Thank you :-)
Bye,
bearophile
Jan 19 2012
next sibling parent reply "Jonathan M Davis" <jmdavisProg gmx.com> writes:
On Thursday, January 19, 2012 17:29:28 bearophile wrote:

 If I am mistaken please I'd like to know why the current design is better
 (or maybe why it's just equally good). Thank you :-)


Honestly, I don't think that the order is all that critical, since all of the 
same assertions are run in either case. But conceptually, the invariant is for 
verifying the state of the object, whereas the post-condition is for verifying 
the state of the return value. And the return value doesn't really matter if 
the object itself just got fried by the function call. Not to mention, if your 
tests of the return value in the post-condition rely on the state of the 
object itself being correct, then your tests in the post-condition aren't 
necessarily going to do what you expect if the invariant would have failed.

I have no idea what Walter's reasoning is though.

- Jonathan M Davis
Jan 19 2012
next sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 1/19/2012 4:08 PM, Jonathan M Davis wrote:

 On Thursday, January 19, 2012 17:29:28 bearophile wrote:

 If I am mistaken please I'd like to know why the current design is better
 (or maybe why it's just equally good). Thank you :-)


 Honestly, I don't think that the order is all that critical, since all of the
 same assertions are run in either case. But conceptually, the invariant is for
 verifying the state of the object, whereas the post-condition is for verifying
 the state of the return value. And the return value doesn't really matter if
 the object itself just got fried by the function call. Not to mention, if your
 tests of the return value in the post-condition rely on the state of the
 object itself being correct, then your tests in the post-condition aren't
 necessarily going to do what you expect if the invariant would have failed.

 I have no idea what Walter's reasoning is though.


My reasoning is it (1) doesn't make any difference and (2) it's always been
like 
that - and if it did make a difference, it would break 10 years of existing
code.
Jan 19 2012
next sibling parent bearophile <bearophileHUGS lycos.com> writes:
Walter:


 My reasoning is it (1) doesn't make any difference and (2) it's always been
like 
 that - and if it did make a difference, it would break 10 years of existing
code.


In the second code example I've shown I receive an assert error in the wrong
place. If a method is buggy, and its post-condition is designed to be able to
catch such bugs, I expect to receive an assert error (or enforcement exception)
with a line number inside the post-condition, and not very far from it into the
invariant.

And my common formal sense tells me that verifying the more general condition
first, tailored to spot errors inside the method that has just run, is better
than doing it in the other order. But I don't know why, formally.

Maybe Eiffel docs explain the order it uses to run pre/post/invariants. I will
try to find how Eiffel is designed here. 
Regarding the breaking, I don't think such change is able to break a lot of D2
code.

Thank you for your answers :-)
Bye,
bearophile
Jan 19 2012
prev sibling parent reply "Steven Schveighoffer" <schveiguy yahoo.com> writes:
On Thu, 19 Jan 2012 20:38:05 -0500, Walter Bright  
<newshound2 digitalmars.com> wrote:


 On 1/19/2012 4:08 PM, Jonathan M Davis wrote:

 On Thursday, January 19, 2012 17:29:28 bearophile wrote:

 If I am mistaken please I'd like to know why the current design is  
 better
 (or maybe why it's just equally good). Thank you :-)


 Honestly, I don't think that the order is all that critical, since all  
 of the
 same assertions are run in either case. But conceptually, the invariant  
 is for
 verifying the state of the object, whereas the post-condition is for  
 verifying
 the state of the return value. And the return value doesn't really  
 matter if
 the object itself just got fried by the function call. Not to mention,  
 if your
 tests of the return value in the post-condition rely on the state of the
 object itself being correct, then your tests in the post-condition  
 aren't
 necessarily going to do what you expect if the invariant would have  
 failed.

 I have no idea what Walter's reasoning is though.


 My reasoning is it (1) doesn't make any difference and (2) it's always  
 been like that - and if it did make a difference, it would break 10  
 years of existing code.


I have to disagree on some level with (1).  It might not make a difference  
in determining there is a bug, but it makes a difference because failing  
in the out-condition gives you more information, even if the invariant is  
broken.  It tells you which function broke the invariant.

Let's say you have a car diagnostic machine which has a choice of  
reporting one of two error codes, a) spark plugs aren't firing, and b) the  
car isn't starting when the key is turned.  Which one would you rather see?

-Steve
Jan 19 2012
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 1/19/2012 6:37 PM, Steven Schveighoffer wrote:

 I have to disagree on some level with (1). It might not make a difference in
 determining there is a bug, but it makes a difference because failing in the
 out-condition gives you more information, even if the invariant is broken. It
 tells you which function broke the invariant.



No, it doesn't give you more information in the out condition. Furthermore, the 
postcondition and the invariant check entirely different state - the return 
value is not the same thing at all as the instance state. There's no reason to 
believe that one is superior to the other, nor that they are redundant.
Jan 19 2012
parent reply "Steven Schveighoffer" <schveiguy yahoo.com> writes:
On Thu, 19 Jan 2012 22:31:08 -0500, Walter Bright  
<newshound2 digitalmars.com> wrote:


 On 1/19/2012 6:37 PM, Steven Schveighoffer wrote:

 I have to disagree on some level with (1). It might not make a  
 difference in
 determining there is a bug, but it makes a difference because failing  
 in the
 out-condition gives you more information, even if the invariant is  
 broken. It
 tells you which function broke the invariant.



 No, it doesn't give you more information in the out condition.  
 Furthermore, the postcondition and the invariant check entirely  
 different state - the return value is not the same thing at all as the  
 instance state. There's no reason to believe that one is superior to the  
 other, nor that they are redundant.


If they are related, yes it does give you more information.  The out  
condition might not check the class data directly, but the error which  
caused the invariant to fail could have also caused the out-condition to  
fail.  It's inconsequential to the *program* whether the out condition or  
the invariant halts execution.  But to the developer receiving the assert  
message, it's much more helpful to see an out condition failing than an  
invariant.  If they are related, and caused by the same bug, it's that  
much more helpful.  Imagine you have 1000 lines of code that call 50 or so  
different methods on a class.  Any one of those calls in any one of those  
methods could cause an invariant failure.  But only one method call can  
cause a specific out condition failure, and the lines of code that call  
that function might be significantly less than 1000 (maybe a handful).

With almost no change to execution speed, semantics, or pretty much  
anything, you will have saved the developer minutes to hours (under the  
right circumstances, maybe even days or weeks) of crappy "how the hell do  
I find this bug" time.  I can't see a single drawback aside from the time  
it takes to test the changes to the compiler.

even your second reason is flawed -- in order for there to be a noticeable  
difference, one would have to make their invariant actually *change* the  
object.  Why do we support that?  In fact, this change would help them  
discover their flawed invariant code :)

-Steve
Jan 19 2012
next sibling parent reply Jonathan M Davis <jmdavisProg gmx.com> writes:
On Thursday, January 19, 2012 23:19:02 Steven Schveighoffer wrote:

 Imagine you have 1000 lines of code that call 50 or so
 different methods on a class.  Any one of those calls in any one of those
 methods could cause an invariant failure.  But only one method call can
 cause a specific out condition failure, and the lines of code that call
 that function might be significantly less than 1000 (maybe a handful).


Won't you be able to see exactly which function failed in the stack trace? Or 
does it not show up, because the invariant is checked _after_ the function 
call? I would still think that the stack trace would make it fairly clear even 
if that's the case.

I don't really care whether the invariant is called first or the post-condition 
is called first though. It just seems more logical to me that the invariant 
would be called first.

- Jonathan M Davis
Jan 19 2012
parent "Steven Schveighoffer" <schveiguy yahoo.com> writes:
On Thu, 19 Jan 2012 23:24:59 -0500, Jonathan M Davis <jmdavisProg gmx.com>  
wrote:


 On Thursday, January 19, 2012 23:19:02 Steven Schveighoffer wrote:

 Imagine you have 1000 lines of code that call 50 or so
 different methods on a class.  Any one of those calls in any one of  
 those
 methods could cause an invariant failure.  But only one method call can
 cause a specific out condition failure, and the lines of code that call
 that function might be significantly less than 1000 (maybe a handful).


 Won't you be able to see exactly which function failed in the stack  
 trace? Or
 does it not show up, because the invariant is checked _after_ the  
 function
 call? I would still think that the stack trace would make it fairly  
 clear even
 if that's the case.


If you get one (that is human decipherable).  This doesn't always happen.   
But like Walter and you said, the order is irrelevant to the execution of  
the program, why make the developer work harder than he has to?  It makes  
no sense to me *not* to change it.

-Steve
Jan 19 2012
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 1/19/2012 8:19 PM, Steven Schveighoffer wrote:

 If they are related, yes it does give you more information. The out condition
 might not check the class data directly, but the error which caused the
 invariant to fail could have also caused the out-condition to fail. It's
 inconsequential to the *program* whether the out condition or the invariant
 halts execution. But to the developer receiving the assert message, it's much
 more helpful to see an out condition failing than an invariant. If they are
 related, and caused by the same bug, it's that much more helpful.


I utterly fail to understand your argument about it being more helpful.



 Imagine you
 have 1000 lines of code that call 50 or so different methods on a class. Any
one
 of those calls in any one of those methods could cause an invariant failure.
But
 only one method call can cause a specific out condition failure, and the lines
 of code that call that function might be significantly less than 1000 (maybe a
 handful).


This does not make sense to me. If a bug would cause an invariant failure and
an 
out failure, and one is run right after the other, there is zero advantage to 
one being run before the other.

    assert(s);
    assert(s);

which one should be run first?


 With almost no change to execution speed, semantics, or pretty much anything,
 you will have saved the developer minutes to hours (under the right
 circumstances, maybe even days or weeks) of crappy "how the hell do I find this
 bug" time.


I see no advantage, even to your hypothetical. I think you would be *very* hard 
pressed to come up with an example.


 I can't see a single drawback aside from the time it takes to test
 the changes to the compiler.


Changing the language requires more than no drawbacks, it requires a compelling 
demonstration of value added.


 even your second reason is flawed -- in order for there to be a noticeable
 difference, one would have to make their invariant actually *change* the
object.
 Why do we support that? In fact, this change would help them discover their
 flawed invariant code :)


Invariants and conditions are allowed to be impure so they can do things like 
logging.
Jan 19 2012
next sibling parent reply Jonathan M Davis <jmdavisProg gmx.com> writes:
On Thursday, January 19, 2012 21:01:40 Walter Bright wrote:

 Invariants and conditions are allowed to be impure so they can do things
 like logging.


Yeah, but if they're modifying state, they're doing something which is 
essentially invalid, so from the standpoint of breaking code, I don't think 
that swapping the order invariants and post-conditions is really an issue. I 
think that it's just a question of which order makes more sense. If that's 
what it is now, then great, we'll leave it as-is. If it's the other way 
around, then I very much doubt that it would negatively impact much code (if 
any) to swap them, since the order really isn't supposed to matter.

- Jonathan M Davis
Jan 19 2012
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 1/19/2012 9:14 PM, Jonathan M Davis wrote:

 Yeah, but if they're modifying state, they're doing something which is
 essentially invalid,


Yup, so arguing for which order the state changes should come in is also
invalid.


 so from the standpoint of breaking code, I don't think
 that swapping the order invariants and post-conditions is really an issue. I
 think that it's just a question of which order makes more sense. If that's
 what it is now, then great, we'll leave it as-is. If it's the other way
 around, then I very much doubt that it would negatively impact much code (if
 any) to swap them, since the order really isn't supposed to matter.


I'm not going to swap them without a compelling demonstration of its
advantages. 
Not breaking much code is not an argument for changing current behavior.
Jan 19 2012
parent reply Manfred Nowak <svv1999 hotmail.com> writes:
Walter Bright wrote:


 I'm not going to swap them without a compelling demonstration of
 its advantages. 


If there are advantages, then the specs are wrong, because they do not 
define the sequence of execution and an optimizing compiler might put 
the calls to <condition>s and `invariant' into different threads 
executed in parallel.

-manfred
Jan 20 2012
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 1/20/2012 12:23 AM, Manfred Nowak wrote:

 If there are advantages, then the specs are wrong,


I recently fixed the specs to define the sequence.
Jan 20 2012
parent reply Manfred Nowak <svv1999 hotmail.com> writes:
Walter Bright wrote:


 I recently fixed the specs to define the sequence.


Then the Status Quo holds. One more remark:

if the intention still is, that contracts are to be seen as an 
executable description of at least parts of the design, then the 
current specification of the language does not give any control over 
those contracts to the designers.

This is because the coder can easily change the contracts and then the 
designer would have a hard time to find that modifications.

This could be changed for eaxmple by compiling the contracts into a 
separate library but seems not to be supported.

Are there other ways to garantie, that the code the coder delivers to 
the designer indeed fulfills the requirements the designer gave before 
handing out the job?
Jan 20 2012
parent Walter Bright <newshound2 digitalmars.com> writes:
On 1/20/2012 10:42 AM, Manfred Nowak wrote:

 if the intention still is, that contracts are to be seen as an
 executable description of at least parts of the design, then the
 current specification of the language does not give any control over
 those contracts to the designers.

 This is because the coder can easily change the contracts and then the
 designer would have a hard time to find that modifications.


D isn't a language that is designed to prevent deliberate subversion - only 
inadvertent subversion.



 This could be changed for eaxmple by compiling the contracts into a
 separate library but seems not to be supported.

 Are there other ways to garantie, that the code the coder delivers to
 the designer indeed fulfills the requirements the designer gave before
 handing out the job?


You can have your contracts call functions in an external library.
Jan 20 2012
prev sibling parent "Steven Schveighoffer" <schveiguy yahoo.com> writes:
On Fri, 20 Jan 2012 00:01:40 -0500, Walter Bright  
<newshound2 digitalmars.com> wrote:


 On 1/19/2012 8:19 PM, Steven Schveighoffer wrote:

 If they are related, yes it does give you more information. The out  
 condition
 might not check the class data directly, but the error which caused the
 invariant to fail could have also caused the out-condition to fail. It's
 inconsequential to the *program* whether the out condition or the  
 invariant
 halts execution. But to the developer receiving the assert message,  
 it's much
 more helpful to see an out condition failing than an invariant. If they  
 are
 related, and caused by the same bug, it's that much more helpful.


 I utterly fail to understand your argument about it being more helpful.


For a class with 50 methods:

invariant error -> one of your 50 methods may have messed up the  
invariant, but I'm not going to tell you which one.  Also, it could have  
been messed up somewhere else, and failed at the beginning of a method  
call, or an extraneous assert.  Have fun looking for where the bug is.
out condition error -> method 25 failed condition at line X.


 Imagine you
 have 1000 lines of code that call 50 or so different methods on a  
 class. Any one
 of those calls in any one of those methods could cause an invariant  
 failure. But
 only one method call can cause a specific out condition failure, and  
 the lines
 of code that call that function might be significantly less than 1000  
 (maybe a
 handful).


 This does not make sense to me. If a bug would cause an invariant  
 failure and an out failure, and one is run right after the other, there  
 is zero advantage to one being run before the other.

     assert(s);
     assert(s);

 which one should be run first?


They are not *located* one right after another.  One is in the invariant  
function which could be called from anywhere, and one is directly attached  
to the code which caused the bug.  Asserts are not only helpful by telling  
you that they failed, but also *where* they failed.  It's not always  
guaranteed that you get a useful stack trace to see where the program is  
running, but you do always get an assert message.


 With almost no change to execution speed, semantics, or pretty much  
 anything,
 you will have saved the developer minutes to hours (under the right
 circumstances, maybe even days or weeks) of crappy "how the hell do I  
 find this
 bug" time.


 I see no advantage, even to your hypothetical. I think you would be  
 *very* hard pressed to come up with an example.


I've had programs that I have written which failed once every 2 weeks.

If such a situation happens, and you just get a single-line assert  
message, then you have to instrument, or run in debugger, wait another 2  
weeks.  Or maybe you get a stack trace without any readable.  Not as bad  
as waiting two weeks, but if you can tell me more information about where  
the program is without me having to get out my stack decoder ring, DO IT!

My philosophy to error reporting is, give me as much information as  
possible about the current state of the program.  Especially for errors  
which are about to make all the evidence go away (aborting errors).  It's  
not perfection, it's not even guaranteed, but do whatever is possible to  
make things easier to figure out without complex tools.

This is a small change for a small gain, but it's a very very simple  
change.  You just reorder one generated call.  The cost is probably less  
than the effort we have expended discussing this.


 even your second reason is flawed -- in order for there to be a  
 noticeable
 difference, one would have to make their invariant actually *change*  
 the object.
 Why do we support that? In fact, this change would help them discover  
 their
 flawed invariant code :)


 Invariants and conditions are allowed to be impure so they can do things  
 like logging.


How does this destroy prior work?  Log messages are slightly out of  
order?  Still not buying it.

-Steve
Jan 20 2012
prev sibling parent reply Davidson Corry <davidsoncorry comcast.net> writes:
On 1/19/2012 4:08 PM, Jonathan M Davis wrote:

 On Thursday, January 19, 2012 17:29:28 bearophile wrote:

 If I am mistaken please I'd like to know why the current design is better
 (or maybe why it's just equally good). Thank you :-)


 Honestly, I don't think that the order is all that critical, since all of the
 same assertions are run in either case. But conceptually, the invariant is for
 verifying the state of the object, whereas the post-condition is for verifying
 the state of the return value. And the return value doesn't really matter if
 the object itself just got fried by the function call. Not to mention, if your
 tests of the return value in the post-condition rely on the state of the
 object itself being correct, then your tests in the post-condition aren't
 necessarily going to do what you expect if the invariant would have failed.

 I have no idea what Walter's reasoning is though.

 - Jonathan M Davis


I certainly can't speak for Walter, either, but to my mind, the 
precondition/invariant/body/invariant/postcondition order makes sense, 
because the object's internal monologue goes like

precondition:  "Does this guy even have any business calling me?"
                (does he meet my method's preconditions?"
invariant:     "Am I in any shape to do the job for him?"
                (do I meet my class invariant, am I a "real" X object?)
body:          Yo.
invariant:     "Am I still in good shape?"
                (did I break something, am I still a valid X?)
postcondition: "Did I do my job, or what?"

Kinda like checking the customer's order to see if we carry those 
widgets (precondition), checking inventory (invariant), getting the 
widget (body), checking inventory again to make sure the books are still 
balanced (invariant), and finally looking to see that what's in my hand 
really is the widget the customer asked for (postcondition), before 
handing the widget over the counter to the customer. That seems like the 
correct order to do things, to me.

Just my opinion.

-- Dai
Jan 19 2012
parent "Steven Schveighoffer" <schveiguy yahoo.com> writes:
On Thu, 19 Jan 2012 22:33:40 -0500, Davidson Corry  
<davidsoncorry comcast.net> wrote:


 On 1/19/2012 4:08 PM, Jonathan M Davis wrote:

 On Thursday, January 19, 2012 17:29:28 bearophile wrote:

 If I am mistaken please I'd like to know why the current design is  
 better
 (or maybe why it's just equally good). Thank you :-)


 Honestly, I don't think that the order is all that critical, since all  
 of the
 same assertions are run in either case. But conceptually, the invariant  
 is for
 verifying the state of the object, whereas the post-condition is for  
 verifying
 the state of the return value. And the return value doesn't really  
 matter if
 the object itself just got fried by the function call. Not to mention,  
 if your
 tests of the return value in the post-condition rely on the state of the
 object itself being correct, then your tests in the post-condition  
 aren't
 necessarily going to do what you expect if the invariant would have  
 failed.

 I have no idea what Walter's reasoning is though.

 - Jonathan M Davis


 I certainly can't speak for Walter, either, but to my mind, the  
 precondition/invariant/body/invariant/postcondition order makes sense,  
 because the object's internal monologue goes like

 precondition:  "Does this guy even have any business calling me?"
                 (does he meet my method's preconditions?"
 invariant:     "Am I in any shape to do the job for him?"
                 (do I meet my class invariant, am I a "real" X object?)
 body:          Yo.
 invariant:     "Am I still in good shape?"
                 (did I break something, am I still a valid X?)
 postcondition: "Did I do my job, or what?"

 Kinda like checking the customer's order to see if we carry those  
 widgets (precondition), checking inventory (invariant), getting the  
 widget (body), checking inventory again to make sure the books are still  
 balanced (invariant), and finally looking to see that what's in my hand  
 really is the widget the customer asked for (postcondition), before  
 handing the widget over the counter to the customer. That seems like the  
 correct order to do things, to me.

 Just my opinion.


The order of checking is irrelevant to the program.  If the invariant is  
going to fail, it's going to fail whether it's checked first or second.   
The only way changing the order could effect a difference is if the  
invariant actually changes the object, and that's invalid code anyway.

But to the developer, an invariant assert could be associated with *any*  
method, whereas an out assert can only be associated with *one* method.   
In cases where both the invariant and the out condition fails, the more  
specific error is more useful for pinpointing a problem (clearly the  
function that has just executed broke the invariant because it passed on  
entry).  It doesn't mean this will always happen, it's quite possibly only  
the invariant fails.  But why specifically avoid exploiting this situation?

The in clause and invariant can execute in either order IMO, because the  
two checks are completely unrelated to the code location of the bug(s)  
(the function in question hasn't been called yet, so that's not where the  
bug is!).

-Steve
Jan 19 2012
prev sibling next sibling parent Mail Mantis <mail.mantis.88 gmail.com> writes:
2012/1/20 bearophile <bearophileHUGS lycos.com>:

 Walter has recently closed a bug report without fixing it and without an =


answer, it's about contract based programming:

 http://d.puremagic.com/issues/show_bug.cgi?id=3D5024

 So I'm asking for more info here.

 As reference I use this little program (I have improved it a bit compared=


 to the one inside issue 5024):

 import std.c.stdio: printf;

 class Foo {
 =A0 =A0int x =3D 0;

 =A0 =A0invariant() {
 =A0 =A0 =A0 =A0printf("Foo invariant: x=3D%d\n", x);
 =A0 =A0 =A0 =A0assert(x >=3D 0);
 =A0 =A0}

 =A0 =A0this() {
 =A0 =A0 =A0 =A0printf("Foo constructor: x=3D%d\n", x);
 =A0 =A0 =A0 =A0x =3D 1;
 =A0 =A0}

 =A0 =A0void setX(int newx)
 =A0 =A0 =A0 =A0in {
 =A0 =A0 =A0 =A0 =A0 =A0printf("Foo.setX precondition: newx=3D%d\n", newx)=


;

 =A0 =A0 =A0 =A0 =A0 =A0assert(newx >=3D 0);
 =A0 =A0 =A0 =A0} out {
 =A0 =A0 =A0 =A0 =A0 =A0printf("Foo.setX postcondition: x=3D%d\n", x);
 =A0 =A0 =A0 =A0 =A0 =A0assert(x =3D=3D newx);
 =A0 =A0 =A0 =A0} body {
 =A0 =A0 =A0 =A0 =A0 =A0printf("Foo.setX body\n");
 =A0 =A0 =A0 =A0 =A0 =A0x =3D newx;
 =A0 =A0 =A0 =A0}
 }

 void main() {
 =A0 =A0auto c =3D new Foo();
 =A0 =A0c.setX(10);
 }



 Currently it prints this, that I don't like:


 Foo constructor: x=3D0
 Foo invariant: x=3D1
 Foo.setX precondition: newx=3D10
 Foo invariant: x=3D1
 Foo.setX body
 Foo invariant: x=3D10
 Foo.setX postcondition: x=3D10



 I'd like this order:

 Foo constructor: x=3D0
 Foo invariant: x=3D1
 Foo invariant: x=3D1
 Foo.setX precondition: newx=3D10
 Foo.setX body
 Foo.setX postcondition: x=3D10
 Foo invariant: x=3D10


 An example of why I think that's better. This is the same program with a =


bug:

 import std.c.stdio: printf;

 class Foo {
 =A0 =A0int x =3D 0;

 =A0 =A0invariant() {
 =A0 =A0 =A0 =A0printf("Foo invariant: x=3D%d\n", x);
 =A0 =A0 =A0 =A0assert(x >=3D 0); // line 8
 =A0 =A0}

 =A0 =A0this() {
 =A0 =A0 =A0 =A0printf("Foo constructor: x=3D%d\n", x);
 =A0 =A0 =A0 =A0x =3D 1;
 =A0 =A0}

 =A0 =A0void setX(int newx)
 =A0 =A0 =A0 =A0in {
 =A0 =A0 =A0 =A0 =A0 =A0printf("Foo.setX precondition: newx=3D%d\n", newx)=


;

 =A0 =A0 =A0 =A0 =A0 =A0assert(newx >=3D 0);
 =A0 =A0 =A0 =A0} out {
 =A0 =A0 =A0 =A0 =A0 =A0printf("Foo.setX postcondition: x=3D%d\n", x);
 =A0 =A0 =A0 =A0 =A0 =A0assert(x =3D=3D newx); // line 22
 =A0 =A0 =A0 =A0} body {
 =A0 =A0 =A0 =A0 =A0 =A0printf("Foo.setX body\n");
 =A0 =A0 =A0 =A0 =A0 =A0x =3D -newx;
 =A0 =A0 =A0 =A0}
 }

 void main() {
 =A0 =A0auto c =3D new Foo();
 =A0 =A0c.setX(10);
 }


 If I run it it gives:
 core.exception.AssertError test2(8): Assertion failure


 So the bug is caught by a the generic invariant at line 8 instead of what=


 I think is the correct place, the setX post-condition at line 22. The post=
-condition is a test meant to verify that the setX() body is correct, while=
 the invariant contains more general tests. So I think it's more right to r=
un the specific tests first, and the more general later.

 If I am mistaken please I'd like to know why the current design is better=


 (or maybe why it's just equally good).

 Thank you :-)
 Bye,
 bearophile


I can think of somewhat this example:

struct Foo {
    int x =3D 1;

    invariant() {
        assert( x >=3D 0 );
    }

    int do_calc( int y )
    in {
        assert( y >=3D 0 );
    } out( result ) {
        assert( result >=3D 0 );
    } body {
        x *=3D -1;     //<- bug
        return x * y;
    }
}

The bug here is caused by accidental object corruption, and invariant
tells that. If assertions are swapped, we will get error at out
contract, which suggests that error is in calculus algorithm.
Jan 19 2012
prev sibling parent Manfred Nowak <svv1999 hotmail.com> writes:
bearophile wrote:


 So I'm asking for more info here.


The classes `invariant' can be eliminated by a `debug'-prefix.

-manfred
Jan 21 2012