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 }