org.jmlspecs.racwrap.runner
Class BranchNode

java.lang.Object
  org.jmlspecs.racwrap.runner.CommonImpl
      org.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

BranchNode

public BranchNode()

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