Create a class with an invariant

Encapsulate the state

A class defines a type; an object is one instance of it. A constructor establishes the initial state. Private fields prevent outside code from assigning directly to the representation, while public methods define the operations that callers may request.

An invariant is a condition the class promises to preserve. Counter keeps value non-negative. Its add method accepts only positive amounts, so callers cannot use it to make the value negative. Each Counter has its own instance field.

public class Demo {
    static class Counter {
        private int value;
        public Counter() { value = 0; }
        public void add(int amount) {
            if (amount > 0) { value += amount; }
        }
        public int getValue() { return value; }
    }
    public static void main(String[] args) {
        Counter first = new Counter();
        Counter second = new Counter();
        first.add(3);
        System.out.println(first.getValue());
        System.out.println(second.getValue());
    }
}

Distinguish instance and class members

An instance method acts on a particular receiver object. A static method belongs to the class and has no implicit receiver. A static field is shared by the class; making value static would cause the counters in this example to share their count.

Test two objects as well as one. Check initialization, a normal update, and an input that should be rejected. Explain preconditions, postconditions, and which methods are responsible for maintaining the invariant.

Check yourself