Invariants for methods

[Jonathan M Davis]

On Thursday, November 18, 2010 09:48:08 Jens Mueller wrote:
> Does it make more sense to talk about an invariant for a member
> function? I mean the member function changes the state of the instance
> but there may be some invariant when changing it. Basically some change
> is allowed but the other isn't.
> struct Rectangle {
> 	// state is only allowed to change in a certain way
> 	// width and height of this Rectangle need to be preserved
>     public void move(...) {
>     }
> 
>     private:
>     State state;
> }
> 
> I'm very thankful for your feedback. At the moment I'm not sure whether
> you see my point.
> I think of an member function invariant as something more fine-grained
> than a class invariant. Of course calling move() needs to preserve the
> class invariant but actually in case of move() it should also do
> something more, namely before calling and after the call the width and
> height should be the same. That's an invariant for the computation of
> move(). How do I express it such that it will be compiled away when
> disabling contracts (i.e. in release mode)?

Ah. I think I get what you're getting at. That strikes me as a bit weird, and I 
wouldn't encourage having that sort of requirement on a function normally, but 
there is no way to have a test which is automatically tested both before and 
after a function call and yet not be in the invariant. You _can_ just put the 
test in both the pre-condition and post-condition. And if that's more code 
duplication than you want, you can create a function which does the test and 
call it in both (or which returns a bool whether the test passed and still youn 
do the assertion in the pre and post-conditions). But regardless, there is no 
way to have a "function invariant" like you're looking for. And generally-
speaking, I wouldn't advise requiring that the member variables of the 
class/struct be required to be in a specific state before a calling a particular 
member function. Sometimes, it's required, but that sort of dependency is likely 
to cause problems more often than not - particularly if it's common for 
functions to have that sort of requirement.

In any case, just put the tests in the in and out blocks, and create a helper 
function if it's too much code duplication.

- Jonathan M Davis