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    }