JML

org.jmlspecs.racwrap.runner
Class BranchNode

java.lang.Object
  extended byorg.jmlspecs.racwrap.runner.CommonImpl
      extended byorg.jmlspecs.racwrap.runner.BranchNode
All Implemented Interfaces:
Node

public class BranchNode
extends CommonImpl
implements Node

BranchNode is an implementation of Node for branches. BranchNode uses nested hashtables to implement Node.


Field Summary
private  Hashtable children
           
 
Fields inherited from class org.jmlspecs.racwrap.runner.CommonImpl
 
Constructor Summary
BranchNode()
           
 
Method Summary
 void addChild(Node n)
          Add a child node to this node.
 Node getChild(String name)
          Given a name, get the child node.
 Enumeration getChildren()
          returns an Enumeration of Nodes, which are this node's children.
 Enumeration getKeys()
          returns an Enumeration of the names of the node's children.
 boolean isEmpty()
          returns true if the node has no children.
 boolean prune()
          removes extraneous nodes.
 void removeChild(String name)
          Does nothing if name is not a child.
 
Methods inherited from class org.jmlspecs.racwrap.runner.CommonImpl
getName, isCheckable, isCheckInvariant, isCheckPostcondition, isCheckPrecondition, isWrap, setCheckable, setCheckInvariant, setCheckPostcondition, setCheckPrecondition, setName, setWrap, toString
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 
Methods inherited from interface org.jmlspecs.racwrap.runner.Node
getName, isCheckable, isCheckInvariant, isCheckPostcondition, isCheckPrecondition, isWrap, setCheckInvariant, setCheckPostcondition, setCheckPrecondition, setName, setWrap
 

Field Detail

children

private Hashtable children
Constructor Detail

BranchNode

public BranchNode()
Method Detail

addChild

public void addChild(Node n)
Description copied from interface: Node
Add a child node to this node.

Specified by:
addChild in interface Node

getChild

public Node getChild(String name)
Description copied from interface: Node
Given a name, get the child node.

Specified by:
getChild in interface Node
Returns:
null if the name is not a child.

getKeys

public Enumeration getKeys()
Description copied from interface: Node
returns an Enumeration of the names of the node's children.

Specified by:
getKeys in interface Node

getChildren

public Enumeration getChildren()
Description copied from interface: Node
returns an Enumeration of Nodes, which are this node's children.

Specified by:
getChildren in interface Node

isEmpty

public boolean isEmpty()
Description copied from interface: Node
returns true if the node has no children.

Specified by:
isEmpty in interface Node

removeChild

public void removeChild(String name)
Description copied from interface: Node
Does nothing if name is not a child.

Specified by:
removeChild in interface Node

prune

public boolean prune()
Description copied from interface: Node
removes extraneous nodes.

Specified by:
prune in interface Node

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.