001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.filespace;
004    
005    
006    /**
007     * A ExtTree is a HashTree that starts out as just a root node, but may
008     * be extended at any time by (recursively) adding children.<p>
009     *
010     * Edges and nodes cannot be deleted once added, however.<p>
011     */
012    
013    class ExtTree extends HashTree {
014    
015        /*
016         * Object invariant: All elements in the edges HashTable are
017         * ExtTrees.
018         */
019    
020    
021        /***************************************************
022         *                                                 *
023         * Creation:                                       *
024         *                                                 *
025         **************************************************/
026    
027        /** Create a root node: */
028        public ExtTree(Object data) {
029            super(data);
030        }
031    
032        /** Create a non-root node: */
033        //@ requires parent != null && label != null;
034        protected ExtTree(Tree parent, String label, Object data) {
035            super(parent, label, data);
036        }
037    
038    
039        /***************************************************
040         *                                                 *
041         * Adding children:                                *
042         *                                                 *
043         **************************************************/
044    
045        /**
046         * Create a new direct child of us with label label and data newData.
047         * The new child will have no direct children.<p>
048         *
049         * If a child by the name of label already exists, then this
050         * routine leaves the tree unchanged.<p>
051         *
052         * In either case, the (resulting) child with label label is returned.<p>
053         */
054        //@ requires label != null;
055        //@ ensures \result != null;
056        public ExtTree addChild(String label, Object newData) {
057            /* Handle case where child already exists: */
058            ExtTree child = (ExtTree)getChild(label);       //@ nowarn Cast;
059            if (child != null) {
060                return child;
061            }
062    
063            child = new ExtTree(this, label, newData);
064            edges.put(label, child);
065            return child;
066        }
067    
068    
069        /**
070         * This is an extended version of addChild that takes a path (a
071         * list of labels) instead of a single label.  It returns the child
072         * located by following path from this node.  It creates any
073         * necessary nodes along the way using addChild with null for
074         * newData.  Path must be non-null.
075         */
076        /*@ requires path != null &&
077            (\forall int i; (0<=i && i<path.length) ==> path[i] != null); */
078        //@ ensures \result != null;
079        public ExtTree addPath(String[] path) {
080            ExtTree currentNode = this;
081    
082            for (int i=0; i<path.length; i++)
083                currentNode = currentNode.addChild(path[i], null);
084            
085            return currentNode;
086        }
087    }