View mode: basic / threaded / horizontal-split · Log in · Help
January 19, 2012
Invariant and pre/post-conditions order
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
January 20, 2012
Re: Invariant and pre/post-conditions order
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
January 20, 2012
Re: Invariant and pre/post-conditions order
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.
January 20, 2012
Re: Invariant and pre/post-conditions order
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
January 20, 2012
Re: Invariant and pre/post-conditions order
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
January 20, 2012
Re: Invariant and pre/post-conditions order
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.
January 20, 2012
Re: Invariant and pre/post-conditions order
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
January 20, 2012
Re: Invariant and pre/post-conditions order
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
January 20, 2012
Re: Invariant and pre/post-conditions order
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
January 20, 2012
Re: Invariant and pre/post-conditions order
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
Top | Discussion index | About this forum | D home