Daikon generated invariant
Class IntTreeSet
/*@ invariant bugfinding.inttreeset.orig.IntTree.BLACK == this.tree.root.color; */
/*@ invariant bugfinding.inttreeset.orig.IntTree.RED == bugfinding.inttreeset.orig.IntTreeSet.$assertionsDisabled; */
/*@ invariant \typeof(this.tree.root) == \type(bugfinding.inttreeset.orig.Range); */
/*@ invariant this.tree.root.parent == null; */
/*@ invariant \typeof(this.tree.root.left) == \type(bugfinding.inttreeset.orig.Range); */
/*@ invariant \typeof(this.tree.root.right) == \type(bugfinding.inttreeset.orig.Range); */
/*@ invariant this.tree.root.color == true; */
/*@ invariant this.tree.root.key >= 0; */
/*@ invariant this.size >= 0; */
/*@ invariant \typeof(this.tree.root) == \typeof(this.tree.root.left); */
/*@ invariant \typeof(this.tree.root) == \typeof(this.tree.root.right); */
/*@ invariant \typeof(this.tree.root.left) == \typeof(this.tree.root.right); */
Class IntTree
/*@ invariant this.root == this.root.left.parent; */
/*@ invariant this.root == this.root.right.parent; */
/*@ invariant this.root.left.parent == this.root.right.parent; */
/*@ invariant this.root.left.left == this.root.right.left; */
/*@ invariant this.root.left.left == this.root.right.right; */
/*@ invariant this.root.left.right == this.root.right.left; */
/*@ invariant this.root.left.right == this.root.right.right; */
/*@ invariant this.root.left.color == this.root.right.color; */
/*@ invariant \typeof(this.root) == \type(bugfinding.inttreeset.orig.Range); */
/*@ invariant this.root.parent == null; */
/*@ invariant \typeof(this.root.left) == \type(bugfinding.inttreeset.orig.Range); */
/*@ invariant \typeof(this.root.left.left) == \type(bugfinding.inttreeset.orig.Range); */
/*@ invariant \typeof(this.root.left.right) == \type(bugfinding.inttreeset.orig.Range); */
/*@ invariant this.root.left.key >= 0; */
/*@ invariant \typeof(this.root.right) == \type(bugfinding.inttreeset.orig.Range); */
/*@ invariant \typeof(this.root.right.left) == \type(bugfinding.inttreeset.orig.Range); */
/*@ invariant \typeof(this.root.right.right) == \type(bugfinding.inttreeset.orig.Range); */
/*@ invariant this.root.right.key >= 2; */
/*@ invariant this.root.key >= 0; */
/*@ invariant \typeof(this.root) == \typeof(this.root.left); */
/*@ invariant \typeof(this.root) == \typeof(this.root.left.left); */
/*@ invariant \typeof(this.root) == \typeof(this.root.left.right); */
/*@ invariant \typeof(this.root) == \typeof(this.root.right); */
/*@ invariant \typeof(this.root) == \typeof(this.root.right.left); */
/*@ invariant \typeof(this.root) == \typeof(this.root.right.right); */
/*@ invariant \typeof(this.root.left) == \typeof(this.root.left.parent); */
/*@ invariant \typeof(this.root.left) == \typeof(this.root.left.left); */
/*@ invariant \typeof(this.root.left) == \typeof(this.root.left.right); */
/*@ invariant \typeof(this.root.left) == \typeof(this.root.right); */
/*@ invariant this.root.left.key < this.root.right.key; */
/*@ invariant this.root.left.key < this.root.key; */
/*@ invariant \typeof(this.root.right) == \typeof(this.root.right.parent); */
/*@ invariant \typeof(this.root.right) == \typeof(this.root.right.left); */
/*@ invariant \typeof(this.root.right) == \typeof(this.root.right.right); */
/*@ invariant this.root.right.key > this.root.key; */
Daikon refined invariant
Below are listed the properties that were maintained after manual inspection. Also, for each property we added validations in the case that some reference is null. For example, the property /*@ invariant this.root.parent == null; */ was rewritten as:
boolean isOK;
if (this.root!=null) {
isOK = this.root.parent == null;
}
Class IntTreeSet
/*@ invariant bugfinding.inttreeset.orig.IntTree.BLACK == this.tree.root.color; */
/*@ invariant this.size >= 0; */
Class IntTree
/*@ invariant this.root == this.root.left.parent; */
/*@ invariant this.root == this.root.right.parent; */
/*@ invariant this.root.left.parent == this.root.right.parent; */
/*@ invariant this.root.left.color == this.root.right.color; */
/*@ invariant this.root.parent == null; */
/*@ invariant this.root.key >= 0; */
/*@ invariant this.root.left.key < this.root.right.key; */
/*@ invariant this.root.left.key < this.root.key; */
/*@ invariant this.root.right.key > this.root.key; */