// $Id: BinaryTree.java,v 1.3 2006/10/10 12:37:30 leavens Exp leavens $

public abstract class BinaryTree {
    public /*@ pure @*/ abstract boolean isLeaf();
    //@ public invariant !isLeaf() ==> this instanceof Interior;

    public abstract int leafSum();

    public static void main(String [] argv) {
        BinaryTree tree_a
            = new Interior(new Leaf(2), "a", new Leaf(3));
        System.out.println(tree_a.leafSum());
    }

}

class Leaf extends BinaryTree {
    private int num;
    public /*@ pure @*/ boolean isLeaf() { return true; }
    public int number() { return num; }
    public Leaf(int n) { num = n; }
    public int leafSum() { return num; }
}

class Interior extends BinaryTree {
    private String sym;
    private BinaryTree left, right;

    //@ private invariant sym != null && left != null && right != null;

    public /*@ pure @*/ boolean isLeaf() { return false; }
    public BinaryTree left_tree() { return left; }
    public BinaryTree right_tree() { return right; }
    public String symbol() { return sym; }

    public int leafSum() {
        return left_tree().leafSum() + right_tree().leafSum();
    }

    //@ requires l != null && s != null && r != null;
    public Interior(BinaryTree l, String s, BinaryTree r) {
        left = l;
        sym = s;
        right = r;
    }
}