An abstract data type of immutable binary trees.

    emptyTree:                   -> Tree
    newTree:   int x Tree x Tree -> Tree
    isEmpty:   Tree              -> boolean
    label:     Tree              -> int
    left:      Tree              -> Tree
    right:     Tree              -> Tree
    height:    Tree              -> int
    size:      Tree              -> int

Algebraic specification:

    isEmpty (emptyTree())          =  true
    isEmpty (newTree (n, t1, t2))  =  false

    label (newTree (n, t1, t2))  =  n
    left  (newTree (n, t1, t2))  =  t1
    right (newTree (n, t1, t2))  =  t2

    height (emptyTree())  =  0
    height (newTree (n, t1, t2))
        =  1 + max (height (t1), height (t2))

    size (emptyTree())  =  0
    size (newTree (n, t1, t2))  =  1 + size (t1) + size (t2)

where max (n1, n2) is the maximum of n1 and n2.

****************************************************************

//  One possible implementation of the Tree ADT in Java.
//  Each operation of the Tree ADT corresponds to a static
//  method of the abstract class Tree.

public abstract class Tree {

    public static Tree emptyTree () {
        return new EmptyTree();
    }

    public static Tree newTree (int n, Tree t1, Tree t2) {
        return new NewTree (n, t1, t2);
    }

    public static boolean isEmpty (Tree t) { return t.isEmpty(); }
    public static int     label   (Tree t) { return t.label(); }
    public static Tree    left    (Tree t) { return t.left(); }
    public static Tree    right   (Tree t) { return t.right(); }
    public static int     height  (Tree t) { return t.height(); }
    public static int     size    (Tree t) { return t.size(); }

    abstract boolean isEmpty ();
    abstract int     label ();
    abstract Tree    left ();
    abstract Tree    right ();
    abstract int     height ();
    abstract int     size ();

    private static class EmptyTree extends Tree {

        EmptyTree () { }

        boolean isEmpty () { return true; }

        int label  () { throw new RuntimeException(); }
        Tree left  ()  { throw new RuntimeException(); }
        Tree right () { throw new RuntimeException(); }
        int height () { return 0; }
        int size () { return 0; }

    }

    private static class NewTree extends Tree {

        NewTree (int n, Tree t1, Tree t2) {
            this.n = n;
            this.t1 = t1;
            this.t2 = t2;
        }

        private int n;
        private Tree t1;
        private Tree t2;

        boolean isEmpty () { return false; }

        int label  () { return n; }
        Tree left  () { return t1; }
        Tree right () { return t2; }

        int height () { return 1 + Math.max (height (t1), height (t2)); }
        int size () { return 1 + size (t1) + size (t2); }

    }

}