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 }