Daikon generated invariant
Class BinomialHeap
/*@ invariant this.Nodes == this.Nodes.child.parent; */
/*@ invariant this.Nodes.parent == this.Nodes.sibling.parent; */
/*@ invariant this.Nodes.key >= 1; */
/*@ invariant this.Nodes.degree >= 0; */
/*@ invariant this.Nodes.parent == null; */
/*@ invariant this.Nodes.sibling.key >= 1; */
/*@ invariant this.Nodes.sibling.degree >= 0; */
/*@ invariant this.Nodes.sibling.parent == null; */
/*@ invariant this.Nodes.child.key >= 1; */
/*@ invariant this.Nodes.child.degree >= 0; */
/*@ invariant this.size >= 0; */
/*@ invariant this.Nodes.key <= this.Nodes.child.key; */
/*@ invariant this.Nodes.degree <= this.Nodes.sibling.degree; */
/*@ invariant this.Nodes.degree - this.Nodes.child.degree - 1 == 0; */
/*@ invariant this.Nodes.degree <= this.size; */
/*@ invariant this.Nodes.sibling.key >= this.Nodes.child.degree; */
/*@ invariant this.Nodes.sibling.degree > this.Nodes.child.degree; */
/*@ invariant this.Nodes.sibling.degree < this.size; */
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.Nodes == this.Nodes.child.parent; */
was rewritten as:
boolean isOK;
if (this.Nodes!=null && this.Nodes.child!=null) {
isOK = this.Nodes == this.Nodes.child.parent;
}
Class BinomialHeap
/*@ invariant this.Nodes == this.Nodes.child.parent; */
/*@ invariant this.Nodes.parent == this.Nodes.sibling.parent; */
/*@ invariant this.Nodes.parent == null; */
/*@ invariant this.Nodes.sibling.parent == null; */
/*@ invariant this.size >= 0; */
/*@ invariant this.Nodes.key <= this.Nodes.child.key; */
/*@ invariant this.Nodes.degree <= this.Nodes.sibling.degree; */
/*@ invariant this.Nodes.degree - this.Nodes.child.degree - 1 == 0; */
/*@ invariant this.Nodes.sibling.degree > this.Nodes.child.degree; */