// $Id: BinaryTree.java,v 1.2 2004/03/11 18:11:07 leavens Exp leavens $

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

    public int leafSum() {
        if (this.isLeaf()) {
            return ((Leaf)this).number();
        } else {
            Interior meAsInterior = (Interior)this;
            return meAsInterior.left_tree().leafSum()
                + meAsInterior.right_tree().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; }
}

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; }

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