Search
Invariant and pre/post-conditions order
Jan 19, 2012
bearophile
Jan 20, 2012
Jonathan M Davis
Jan 20, 2012
Walter Bright
Jan 20, 2012
bearophile
Jan 20, 2012
Walter Bright
Jan 20, 2012
Jonathan M Davis
Jan 20, 2012
Walter Bright
Jan 20, 2012
Jonathan M Davis
Jan 20, 2012
Walter Bright
Jan 20, 2012
Manfred Nowak
Jan 20, 2012
Walter Bright
Jan 20, 2012
Manfred Nowak
Jan 20, 2012
Walter Bright
Jan 20, 2012
Davidson Corry
Jan 20, 2012
Mail Mantis
Jan 21, 2012
Manfred Nowak
```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

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

Bye,
bearophile
```
```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
```
```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.
```
```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
```
```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
```
```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
```
```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
```
« First   ‹ Prev
1 2 3