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 }