---

Unit.java

public class Unit {
    public static void main(String[] args) {
        int x;
        A a = new ImpA();
        x = a.foo(0);
        B b = new ImpB();
        x = b.foo(0);
        C c = new ImpC();
        x = c.foo(0);
        D d = new ImpD();
        x = d.foo(0);
        E e = new ImpE();
        x = e.foo(0);
        F f = new ImpF();
        x = f.foo(0);
        G g = new ImpG();
        x = g.foo(0);
    }
}

interface A {
    /**
     * @observable
     *   INVOKE XEq0(this): x == 0;
     *   RETURN XEq1(this): $ret == 0;
     */
    public int foo(int x);
}

interface B extends A {
}

interface C extends A {
}

interface D extends B {
}

interface E extends B {
}

interface F extends C {
}

interface G extends C {
}

/**
 *
 * @observable
 *   EXP XEq0or1(this): x == 0 || x == 1;
 */
class ImpA implements A {
    int x;
    public int foo(int x) {
        this.x = x + 1;
        return this.x;
    }
}

class ImpB extends ImpA implements B {
    int x;
    public int foo(int x) {
        if (x != 0) {
            this.x = 0;
        } else {
            this.x = 1;
        }
        return this.x;
    }
}

class ImpC extends ImpA implements C {
}

class ImpD extends ImpB implements D {
}

class ImpE extends ImpB implements E {
}

class ImpF extends ImpC implements F {
}

class ImpG extends ImpC implements G {
}

---