Invariants for methods

[Jens Mueller]

Jonathan M Davis wrote:
> On Thursday 18 November 2010 06:09:33 Jens Mueller wrote:
> > Hi,
> > 
> > I'm wondering what's a good way to do invariants for methods. In my
> > example I have a rectangle and one of its methods moves the upper left
> > of the rectangle. I have two invariants when moving a rectangle: The
> > width and the height do not change. I could do something like the
> > following:
> > 
> > void move(...) {
> >     int currentWidth = width;
> >     int currentHeight = height;
> >     // moving the rectangle here
> >     assert(currentWidth == width);
> >     assert(currentHeight == height);
> > }
> > 
> > I do not like it because it won't be completely compiled away in release
> > mode. The problem is that in the out contract I cannot access variables
> > of the in contract. If that was possible it just becomes:
> > in {
> >     int currentWidth = width;
> >     int currentHeight = height;
> > }
> > out {
> >     assert(currentWidth == width);
> >     assert(currentHeight == height);
> > }
> > body {
> >     // moving the rectangle here
> > }
> > 
> > Is there a solution that works right now? Are their plans to support
> > something like the above? Or should I do it differently?
> 
> in blocks define prefix conditions. They can test arguments to the function, 
> global variables, and members of the class/struct that the function is a member 
> of (if it's a member of one).
> 
> out blocks define postfix conditions. They can test the return value of a function 
> (assuming that you use out(result) instead of just out), global variables, and 
> members of the class/struct that the function is a member of (if it's a member 
> of one).
> 
> An invariant() block defines an invariant for a class or struct and is called 
> before and after every public member function call. It has access to the 
> class/struct and global variables (why it requires parens, I don't know).
> 
> It makes no sense to talk about an invariant for a function however. All of a 
> function's input can be tested with its in block (including global variables and 
> member variables if you need to), and all of a function's output can be tested 
> with its out block (including global variables and member variables if you need 
> to). The only thing left would be checking the function's local variables, but 
> they obviously don't exist in the in or out block, and they don't matter outside 
> of the function itself. If you care about testing them as you do whatever 
> calculations that you're doing in the function, then you can use asserts within 
> the function.

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)?

Jens