JML

org.jmlspecs.samples.sets
Class IntegerSetAsTree

java.lang.Object
  extended byorg.jmlspecs.samples.sets.IntegerSetAsTree
All Implemented Interfaces:
IntegerSetInterface

public class IntegerSetAsTree
extends Object
implements IntegerSetInterface

Sets of integers implemented as binary search trees. This implementation demonstrates the use of JML's helper modifier.

Author:
Katie Becker, Gary T. Leavens, Arthur Thomas

Field Summary
private  boolean isEmpty
          Is this tree empty?
private  IntegerSetAsTree left
          The left subtree, which may be null.
private  IntegerSetAsTree parent
          The parent of this subtree, which may be null.
private  IntegerSetAsTree right
          The right subtree, which may be null.
private  int rootValue
          The integer at the root of the set.
 
Constructor Summary
  IntegerSetAsTree()
          Initialize this integer set to be empty.
protected IntegerSetAsTree(int elem, IntegerSetAsTree par)
           
 
Method Summary
private  void constrHelper()
          Set the left and right to null.
private  IntegerSetAsTree getPredecessor()
           
private  IntegerSetAsTree getSuccessor()
           
 void insert(int elem)
          Insert the given integer into this set.
private  boolean isLeftChild()
          Is this node and left child of its parent?.
 boolean isMember(int elem)
          Tell if the argument is in this set.
protected  String printTree(boolean isFirst)
           
 void remove(int elem)
          Remove the given integer from this set.
private  void removeHelper(int elem)
          Remove the given integer from this set.
private  void removeLeaf()
          Remove an integer from a leaf node.
private  void removeRoot()
          Replace the current node with the successor or predecessor.
 String toString()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

isEmpty

private boolean isEmpty
Is this tree empty? When this is true, rootValue is not defined.


rootValue

private int rootValue
The integer at the root of the set.


left

private IntegerSetAsTree left
The left subtree, which may be null.


right

private IntegerSetAsTree right
The right subtree, which may be null.


parent

private IntegerSetAsTree parent
The parent of this subtree, which may be null.

Constructor Detail

IntegerSetAsTree

public IntegerSetAsTree()
Initialize this integer set to be empty.


IntegerSetAsTree

protected IntegerSetAsTree(int elem,
                           IntegerSetAsTree par)
Method Detail

constrHelper

private void constrHelper()
Set the left and right to null.


insert

public void insert(int elem)
Description copied from interface: IntegerSetInterface
Insert the given integer into this set.

Specified by:
insert in interface IntegerSetInterface

isMember

public boolean isMember(int elem)
Description copied from interface: IntegerSetInterface
Tell if the argument is in this set.

Specified by:
isMember in interface IntegerSetInterface

remove

public void remove(int elem)
Description copied from interface: IntegerSetInterface
Remove the given integer from this set.

Specified by:
remove in interface IntegerSetInterface

removeHelper

private void removeHelper(int elem)
Remove the given integer from this set. Note that the invariants don't all apply to this method. That is important, because the tree surgery done by this method calls this method recursively in states in which the invariant does not hold.


removeRoot

private void removeRoot()
Replace the current node with the successor or predecessor.


removeLeaf

private void removeLeaf()
Remove an integer from a leaf node.


isLeftChild

private boolean isLeftChild()
Is this node and left child of its parent?.


getSuccessor

private IntegerSetAsTree getSuccessor()

getPredecessor

private IntegerSetAsTree getPredecessor()

toString

public String toString()
Overrides:
toString in class Object

printTree

protected String printTree(boolean isFirst)

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.