org.jmlspecs.samples.sets
Class IntegerSetAsTree

java.lang.Object
  org.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

Class Specifications

private invariant (this.left != null||this.right != null) ==> !this.isEmpty; private invariant this.left != null ==> ( \forall org.jmlspecs.models.JMLInteger i; i != null&&this.left.theSet.has(i); i.intValue() < this.rootValue); private invariant this.right != null ==> ( \forall org.jmlspecs.models.JMLInteger i; i != null&&this.right.theSet.has(i); this.rootValue < i.intValue()); private invariant this.parent != null ==> !this.parent.isEmpty; private invariant this.parent != null&&this.parent.left != null ==> this.parent.left.rootValue < this.parent.rootValue; private invariant this.parent != null&&this.parent.right != null ==> this.parent.rootValue < this.parent.right.rootValue; private invariant this.left != null ==> !this.left.isEmpty&&this.left.rootValue < this.rootValue; private invariant this.right != null ==> !this.right.isEmpty&&this.rootValue < this.right.rootValue; private represents theSet <- this.abstractValue();

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Specifications inherited from interface IntegerSetInterface

instance public invariant_redundantly this.theSet != null; instance public invariant ( \forall org.jmlspecs.models.JMLType e; this.theSet.has(e); e instanceof org.jmlspecs.models.JMLInteger); public initially this.theSet.isEmpty();

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface org.jmlspecs.samples.sets.IntegerSetInterface

theSet

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

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)

 

Model Method Summary
JMLValueSet	abstractValue()           Return the abstract value of this IntegerSetAsTree.

 

Model methods inherited from class java.lang.Object

hashValue

 

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.

Specifications:
is in groups: theSet

rootValue

private int rootValue

The integer at the root of the set.

Specifications:
is in groups: theSet

left

private IntegerSetAsTree left

The left subtree, which may be null.

Specifications: nullable
is in groups: theSet
maps left.theSet \into theSet

right

private IntegerSetAsTree right

The right subtree, which may be null.

Specifications: nullable
is in groups: theSet
maps right.theSet \into theSet

parent

private IntegerSetAsTree parent

The parent of this subtree, which may be null.

Specifications: nullable
is in groups: theSet

IntegerSetAsTree

public IntegerSetAsTree()

Initialize this integer set to be empty.

Specifications:

public normal_behavior
assignable theSet;
ensures this.theSet.isEmpty();

IntegerSetAsTree

protected IntegerSetAsTree(int elem,
                           IntegerSetAsTree par)

Specifications:

protected normal_behavior
assignable theSet;
ensures this.theSet.equals(new org.jmlspecs.models.JMLValueSet(new org.jmlspecs.models.JMLInteger(elem)));

abstractValue

public JMLValueSet abstractValue()

Return the abstract value of this IntegerSetAsTree.

Specifications: pure

ensures \result != null;

constrHelper

private void constrHelper()

Set the left and right to null.

Specifications: helper

private normal_behavior
assignable theSet;
ensures this.left == null&&this.right == null;
ensures \not_modified(isEmpty)&&\not_modified(parent);
ensures \not_modified(rootValue);

insert

public void insert(int elem)

Description copied from interface: IntegerSetInterface

Insert the given integer into this set.

Specified by:

insert in interface IntegerSetInterface

Specifications inherited from overridden method insert(int elem) in interface IntegerSetInterface:

public normal_behavior
assignable theSet;
ensures this.theSet.equals(\old(this.theSet.insert(new org.jmlspecs.models.JMLInteger(elem))));

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

Specifications: pure

Specifications inherited from overridden method isMember(int elem) in interface IntegerSetInterface:
       pure

public normal_behavior
ensures \result == this.theSet.has(new org.jmlspecs.models.JMLInteger(elem));

remove

public void remove(int elem)

Description copied from interface: IntegerSetInterface

Remove the given integer from this set.

Specified by:

remove in interface IntegerSetInterface

Specifications inherited from overridden method remove(int elem) in interface IntegerSetInterface:

public normal_behavior
assignable theSet;
ensures this.theSet.equals(\old(this.theSet.remove(new org.jmlspecs.models.JMLInteger(elem))));

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.

Specifications: helper

private normal_behavior
assignable theSet;
ensures this.theSet.equals(\old(this.theSet.remove(new org.jmlspecs.models.JMLInteger(elem))));

removeRoot

private void removeRoot()

Replace the current node with the successor or predecessor.

Specifications: helper

requires this.left != null||this.right != null;
assignable theSet;

removeLeaf

private void removeLeaf()

Remove an integer from a leaf node.

Specifications: helper

requires this.left == null&&this.right == null;

{|

requires this.parent != null;
assignable parent.theSet, isEmpty;

also

requires this.parent == null;
assignable isEmpty;

|}

isLeftChild

private boolean isLeftChild()

Is this node and left child of its parent?.

Specifications: pure helper

requires this.parent != null;

getSuccessor

private IntegerSetAsTree getSuccessor()

Specifications: pure nullable helper

requires this.right == null;
ensures \result == null;

     also

requires this.right != null;
ensures \result != null&&\result .theSet.has(new org.jmlspecs.models.JMLInteger(( \min int i; this.right.theSet.has(new org.jmlspecs.models.JMLInteger(i)); i)));

getPredecessor

private IntegerSetAsTree getPredecessor()

Specifications: pure nullable helper

requires this.left == null;
ensures \result == null;

     also

requires this.left != null;
ensures \result != null&&\result .theSet.has(new org.jmlspecs.models.JMLInteger(( \max int i; this.left.theSet.has(new org.jmlspecs.models.JMLInteger(i)); i)));

toString

public String toString()

Overrides:

toString in class Object

Specifications: pure

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;

printTree

protected String printTree(boolean isFirst)

Specifications: pure

protected normal_behavior
assignable \nothing;
ensures \result != null;