Invariants for methods

[Jonathan M Davis]

On Thursday, November 18, 2010 10:03:16 Jonathan M Davis wrote:
> 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.

Ah. Only closer inspection. I see that I still misunderstood what you meant. I 
thought that you meant that you wanted a particular thing to be true before and 
after the function call but not necessarily be true for all function calls in 
the class/struct. I should have read more carefully.

Andrei's suggestion is a good one.

- Jonathan M Davis