Contracts and inner classes - Abnaxos/contracts GitHub Wiki

Unfortunately, inner/nested classes and contracts don't play very well together. The fact that inner classes or nested may access private members of its enclosing classes causes some serious obscurity about when post and preconditions apply and when they don't. Obviously, this is especially difficult with invariants.

An example:

@Invariant("value>0")
public class Foo {
    private int value = 42;

    public int getValue() {
        return value;
    }

    public Bar newBar() {
        return new Bar();
    }

    public class Bar {
        private Bar() {
        }
        public void doSomething() {
            value = -42;
        }
    }
}

myFoo.newBar().doSomething() will now cause a class state inconsistent with the contract (value must be greater than 0).

Well, in this case, this can be resolved rather easily: Because Bar is an inner class of Foo, we can just define that invariants will also be checked on entry and exit of methods of inner classes. This seems like a good idea anyway.

But let's change the above code a litte bit and make Bar a nested class:

@Invariant("value>0")
public class Foo {
    private int value = 42;

    public int getValue() {
        return value;
    }

    public Bar newBar() {
        return new Bar();
    }

    public static class Bar {
        private Bar() {
        }
        public void doSomething(Foo foo) {
            foo.value = -42;
        }
    }
}

Now we've got a problem. :(

Possible Solutions

• Annotate such invariants on fields. This may have a massive performance impact. Also, invariants may sometimes depend on methods. The compiler generates and uses accessor methods to access private fields and methods. This makes things a lot easier: Check invariants there. ;) Tending to do exactly this.

  This also implies that inner or nested classes have no way to temporarily violate the contract of the enclosing class. Well, you'll have to provide private methods in the enclosing class if you need to do this. Problem solved.

• Detect that Foo has been accessed this way and check invariants on method exit. Seems to be the nicest solution, bit it's probably not exactly trivial to do.

• Ignore it: The programmer should know what he's doing when fiddling around with private members. ;) The contract violation will be reported on the next method entry from the outside.