Invariant and pre/post-conditions order

[Steven Schveighoffer]

On Thu, 19 Jan 2012 22:33:40 -0500, Davidson Corry  
<davidsoncorry at 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