Training Binary Classifiers as Data Structure Invariants

Daikon in the Fibonacci Heap case

Daikon generated invariant

Class FibonacciHeap

/*@ invariant this.min == this.min.right.left; */

/*@ invariant this.min.parent == this.min.child; */

/*@ invariant this.min.parent == this.min.right.parent; */

/*@ invariant this.min.parent == this.min.right.child; */

/*@ invariant this.min.parent == this.min.left.parent; */

/*@ invariant this.min.parent == this.min.left.child; */

/*@ invariant this.min.right.left == this.min.left.right; */

/*@ invariant this.min.right.degree == this.min.degree; */

/*@ invariant this.min.right.mark == this.min.mark; */

/*@ invariant this.min.left.degree == this.min.degree; */

/*@ invariant this.min.left.mark == this.min.mark; */

/*@ invariant this.min.key >= 0; */

/*@ invariant this.min.parent == null; */

/*@ invariant this.min.right.key >= 0; */

/*@ invariant this.min.left.key >= 0; */

/*@ invariant this.min.degree == 0; */

/*@ invariant this.min.mark == false; */

/*@ invariant this.n >= 0; */

/*@ invariant this.min.key <= this.min.right.key; */

/*@ invariant this.min.key <= this.min.left.key; */

/*@ invariant this.min.key >= this.min.degree; */

/*@ invariant this.min.right.key >= this.min.degree; */

/*@ invariant this.min.left.key >= this.min.degree; */

/*@ invariant this.min.degree % this.n == 0; */

/*@ invariant this.min.degree < this.n; */

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.min.parent == this.min.child; */

was rewritten as:

boolean isOK;

if (this.min!=null) {

isOK = this.min.parent == this.min.child;

}