    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package javafe.filespace;
    004
    005
    006    import java.util.Enumeration;
    007    import java.util.Hashtable;
    008
    009
    010    /**
    011     * A HashTree is a Tree that uses a Hashtable to store the map between
    012     * labels and its direct children.<p>
    013     *
    014     * This abstract class leaves how the Hashtable should be filled up to its
    015     * subclasses.<p>
    016     */
    017
    018    abstract class HashTree extends Tree {
    019
    020        /***************************************************
    021         *                                                 *
    022         * Instance variables:                             *
    023         *                                                 *
    024         **************************************************/
    025
    026        /**
    027         * The mapping between our outgoing edge's labels and the subTrees
    028         * they point to.  No entry for a label means no edge with that
    029         * label exists.<p>
    030         *
    031         * Invariant: all elements of edges are Trees and all keys are
    032         * Strings.<p>
    033         */
    034        //+@ invariant edges.keyType == \type(String);
    035        //+@ invariant edges.elementType == \type(Tree);
    036        protected /*@ non_null @*/ Hashtable edges = new Hashtable(5);
    037
    038
    039        /***************************************************
    040         *                                                 *
    041         * Creation:                                       *
    042         *                                                 *
    043         **************************************************/
    044
    045        /** Create a root node: */
    046        public HashTree(Object data) {
    047            super(data);
    048
    049            //+@ set edges.keyType = \type(String);
    050            //+@ set edges.elementType = \type(Tree);
    051        }
    052
    053        /** Create a non-root node: */
    054        protected HashTree(/*@ non_null @*/ Tree parent,
    055                           /*@ non_null @*/ String label,
    056                           Object data) {
    057            super(parent, label, data);
    058
    059            //+@ set edges.keyType = \type(String);
    060            //+@ set edges.elementType = \type(Tree);
    061        }
    062
    063
    064        /***************************************************
    065         *                                                 *
    066         * Fetching children:                              *
    067         *                                                 *
    068         **************************************************/
    069
    070        /**
    071         * An enumeration of this node's direct children.  Each child
    072         * occurs exactly once in the enumeration.  The order is
    073         * unspecified and may differ from call to call.<p>
    074         *
    075         * Note: The Objects returned by the resulting enumeration's
    076         * nextElement method are guaranteed to be of type Tree and non-null.<p>
    077         */
    078        public Enumeration children() {
    079            return edges.elements();
    080        }
    081
    082
    083        /**
    084         * Fetch our direct child along the edge labelled label.  Iff there
    085         * is no such child, return null.
    086         */
    087        public Tree getChild(String label) {
    088            return (Tree)edges.get(label);
    089        }
    090    }