Daikon generated invariant
Class BinTree
/*@ invariant this.root.left.key>= 0; */
/*@ invariant this.root.right.key >= 1; */
/*@ invariant this.root.key >= 0; */
/*@ invariant this.size >= 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 */
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.left.key < this.root.right.key; */
was rewritten as:
boolean isOK;
if (this.root!=null && this.root.left!=null && this.root.right!=null) {
isOK = this.root.left.key < this.root.right.key;
}
Class BinTree
/*@ invariant this.size >= 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 */