Daikon generated invariant
Class Schedule
/*@ invariant this.MAXPRIO == this.prioQueue.length-1; */
/*@ invariant this.allocProcNum == this.numProcesses; */
/*@ invariant this.curProc.next.priority == this.curProc.priority; */
/*@ invariant this.MAXPRIO == 3; */
/*@ invariant this.allocProcNum >= 0; */
/*@ invariant this.curProc.next.val >= 1; */
/*@ invariant this.curProc.next.priority == 1 || this.curProc.next.priority == 2 || this.curProc.next.priority == 3; */
/*@ invariant this.curProc.prev == null; */
/*@ invariant this.curProc.val >= 0; */
/*@ invariant this.curProc.priority == 1 || this.curProc.priority == 2 || this.curProc.priority == 3; */
/*@ invariant \typeof(this.prioQueue) == \type(bugfinding.schedule.orig.List[]); */
/*@ invariant this.blockQueue == null; */
/*@ invariant this.prioQueue.length == 4; */
/*@ invariant this.prioQueue[this.curProc.next.priority] != null; */
/*@ invariant this.prioQueue[this.curProc.priority] != null; */
/*@ invariant this.MAXPRIO >= this.curProc.next.priority; */
/*@ invariant this.MAXPRIO >= this.curProc.priority; */
/*@ invariant this.allocProcNum > this.curProc.next.val; */
/*@ invariant this.allocProcNum > this.curProc.val; */
/*@ invariant this.curProc.next.val > this.curProc.val; */
/*@ invariant this.curProc.next.priority % this.curProc.priority == 0; */
/*@ invariant this.curProc.priority % this.curProc.next.priority == 0; */
/*@ invariant this.curProc.next.priority <= this.prioQueue.length-1; */
/*@ invariant this.curProc.priority <= this.prioQueue.length-1; */
/*@ invariant !(\forall int i; (0 <= i && i <= this.prioQueue.length-1) ==> (this.prioQueue[i] != this.blockQueue)); */
/*@ invariant prioQueue.owner == this; */
Class Job
/*@ invariant this.next == this.next.next.prev; */
/*@ invariant this.next == this.next.prev.next; */
/*@ invariant this.next == this.prev.next.next; */
/*@ invariant this.next.next.prev == this.next.prev.next; */
/*@ invariant this.next.next.prev == this.prev.next.next; */
/*@ invariant this.next.next.priority == this.next.prev.priority; */
/*@ invariant this.next.next.priority == this.next.priority; */
/*@ invariant this.next.next.priority == this.prev.next.priority; */
/*@ invariant this.next.next.priority == this.prev.priority; */
/*@ invariant this.next.next.priority == this.priority; */
/*@ invariant this.next.prev == this.prev.next; */
/*@ invariant this.next.prev.next == this.prev.next.next; */
/*@ invariant this.next.prev.prev == this.prev; */
/*@ invariant this.next.prev.prev == this.prev.next.prev; */
/*@ invariant this.next.prev.prev == this.prev.prev.next; */
/*@ invariant this.next.prev.val == this.prev.next.val; */
/*@ invariant this.next.prev.val == this.val; */
/*@ invariant this.next.prev.priority == this.next.priority; */
/*@ invariant this.next.prev.priority == this.prev.next.priority; */
/*@ invariant this.next.prev.priority == this.prev.prev.priority; */
/*@ invariant this.next.prev.priority == this.prev.priority; */
/*@ invariant this.next.prev.priority == this.priority; */
/*@ invariant this.next.priority == this.prev.next.priority; */
/*@ invariant this.next.priority == this.prev.prev.priority; */
/*@ invariant this.next.priority == this.prev.priority; */
/*@ invariant this.next.priority == this.priority; */
/*@ invariant this.prev == this.prev.next.prev; */
/*@ invariant this.prev == this.prev.prev.next; */
/*@ invariant this.prev.next.prev == this.prev.prev.next; */
/*@ invariant this.prev.next.val == this.val; */
/*@ invariant this.prev.next.priority == this.prev.prev.priority; */
/*@ invariant this.prev.next.priority == this.prev.priority; */
/*@ invariant this.prev.next.priority == this.priority; */
/*@ invariant this.prev.prev.priority == this.prev.priority; */
/*@ invariant this.prev.prev.priority == this.priority; */
/*@ invariant this.prev.priority == this.priority; */
/*@ invariant this.next.next.val >= 2; */
/*@ invariant this.next.next.priority == 1 || this.next.next.priority == 2 || this.next.next.priority == 3; */
/*@ invariant this.next.prev.val >= 0; */
/*@ invariant this.next.prev.priority == 1 || this.next.prev.priority == 2 || this.next.prev.priority == 3; */
/*@ invariant this.next.val >= 1; */
/*@ invariant this.next.priority == 1 || this.next.priority == 2 || this.next.priority == 3; */
/*@ invariant this.prev.next.val >= 1; */
/*@ invariant this.prev.next.priority == 1 || this.prev.next.priority == 2 || this.prev.next.priority == 3; */
/*@ invariant this.prev.prev.val >= 0; */
/*@ invariant this.prev.prev.priority == 1 || this.prev.prev.priority == 2 || this.prev.prev.priority == 3; */
/*@ invariant this.prev.val >= 0; */
/*@ invariant this.prev.priority == 1 || this.prev.priority == 2 || this.prev.priority == 3; */
/*@ invariant this.val >= 0; */
/*@ invariant this.priority >= 0; */
/*@ invariant this.next.next.val > this.next.prev.val; */
/*@ invariant this.next.next.val > this.next.val; */
/*@ invariant this.next.next.val > this.prev.next.val; */
/*@ invariant this.next.next.val >= this.prev.next.priority; */
/*@ invariant this.next.next.val > this.prev.val; */
/*@ invariant this.next.next.val >= this.prev.priority; */
/*@ invariant this.next.next.val > this.val; */
/*@ invariant this.next.next.priority % this.next.prev.priority == 0; */
/*@ invariant this.next.prev.priority % this.next.next.priority == 0; */
/*@ invariant this.next.next.priority % this.next.priority == 0; */
/*@ invariant this.next.priority % this.next.next.priority == 0; */
/*@ invariant this.next.next.priority % this.prev.next.priority == 0; */
/*@ invariant this.prev.next.priority % this.next.next.priority == 0; */
/*@ invariant this.next.next.priority % this.prev.priority == 0; */
/*@ invariant this.prev.priority % this.next.next.priority == 0; */
/*@ invariant this.next.next.priority % this.priority == 0; */
/*@ invariant this.priority % this.next.next.priority == 0; */
/*@ invariant this.next.prev.val < this.next.val; */
/*@ invariant this.next.prev.val > this.prev.prev.val; */
/*@ invariant this.next.prev.val > this.prev.val; */
/*@ invariant this.next.prev.priority % this.next.priority == 0; */
/*@ invariant this.next.priority % this.next.prev.priority == 0; */
/*@ invariant this.next.prev.priority % this.prev.next.priority == 0; */
/*@ invariant this.prev.next.priority % this.next.prev.priority == 0; */
/*@ invariant this.next.prev.priority % this.prev.prev.priority == 0; */
/*@ invariant this.prev.prev.priority % this.next.prev.priority == 0; */
/*@ invariant this.next.prev.priority % this.prev.priority == 0; */
/*@ invariant this.prev.priority % this.next.prev.priority == 0; */
/*@ invariant this.next.prev.priority % this.priority == 0; */
/*@ invariant this.priority % this.next.prev.priority == 0; */
/*@ invariant this.next.val > this.prev.next.val; */
/*@ invariant this.next.val > this.prev.prev.val; */
/*@ invariant this.next.val >= this.prev.prev.priority; */
/*@ invariant this.next.val > this.prev.val; */
/*@ invariant this.next.val > this.val; */
/*@ invariant this.next.priority % this.prev.next.priority == 0; */
/*@ invariant this.prev.next.priority % this.next.priority == 0; */
/*@ invariant this.next.priority % this.prev.prev.priority == 0; */
/*@ invariant this.prev.prev.priority % this.next.priority == 0; */
/*@ invariant this.next.priority % this.prev.priority == 0; */
/*@ invariant this.prev.priority % this.next.priority == 0; */
/*@ invariant this.next.priority % this.priority == 0; */
/*@ invariant this.priority % this.next.priority == 0; */
/*@ invariant this.prev.next.val > this.prev.prev.val; */
/*@ invariant this.prev.next.val > this.prev.val; */
/*@ invariant this.prev.next.priority % this.prev.prev.priority == 0; */
/*@ invariant this.prev.prev.priority % this.prev.next.priority == 0; */
/*@ invariant this.prev.next.priority % this.prev.priority == 0; */
/*@ invariant this.prev.priority % this.prev.next.priority == 0; */
/*@ invariant this.prev.next.priority % this.priority == 0; */
/*@ invariant this.priority % this.prev.next.priority == 0; */
/*@ invariant this.prev.prev.val < this.prev.val; */
/*@ invariant this.prev.prev.val < this.val; */
/*@ invariant this.prev.prev.priority % this.prev.priority == 0; */
/*@ invariant this.prev.priority % this.prev.prev.priority == 0; */
/*@ invariant this.prev.prev.priority % this.priority == 0; */
/*@ invariant this.priority % this.prev.prev.priority == 0; */
/*@ invariant this.prev.val < this.val; */
/*@ invariant this.prev.priority % this.priority == 0; */
/*@ invariant this.priority % this.prev.priority == 0; */
Class List
/*@ invariant this.first.next.priority == this.first.priority; */
/*@ invariant this.first.next.priority == this.last.next.priority; */
/*@ invariant this.first.next.priority == this.last.prev.priority; */
/*@ invariant this.first.next.priority == this.last.priority; */
/*@ invariant this.first.prev == this.last.next.next; */
/*@ invariant this.first.priority == this.last.next.priority; */
/*@ invariant this.first.priority == this.last.prev.priority; */
/*@ invariant this.first.priority == this.last.priority; */
/*@ invariant this.last == this.last.next.prev; */
/*@ invariant this.last == this.last.prev.next; */
/*@ invariant this.last.next.prev == this.last.prev.next; */
/*@ invariant this.last.next.priority == this.last.prev.priority; */
/*@ invariant this.last.next.priority == this.last.priority; */
/*@ invariant this.last.prev.priority == this.last.priority; */
/*@ invariant this.first.next.val >= 1; */
/*@ invariant this.first.next.priority == 1 || this.first.next.priority == 2 || this.first.next.priority == 3; */
/*@ invariant this.first.prev == null; */
/*@ invariant this.first.val >= 0; */
/*@ invariant this.first.priority == 1 || this.first.priority == 2 || this.first.priority == 3; */
/*@ invariant this.last.next.next == null; */
/*@ invariant this.last.next.val >= 1; */
/*@ invariant this.last.next.priority == 1 || this.last.next.priority == 2 || this.last.next.priority == 3; */
/*@ invariant this.last.prev.val >= 0; */
/*@ invariant this.last.prev.priority == 1 || this.last.prev.priority == 2 || this.last.prev.priority == 3; */
/*@ invariant this.last.val >= 0; */
/*@ invariant this.last.priority == 1 || this.last.priority == 2 || this.last.priority == 3; */
/*@ invariant this.memCount >= 0; */
/*@ invariant this.first.next.val > this.first.val; */
/*@ invariant this.first.next.val <= this.last.next.val; */
/*@ invariant this.first.next.priority % this.first.priority == 0; */
/*@ invariant this.first.priority % this.first.next.priority == 0; */
/*@ invariant this.first.next.priority % this.last.next.priority == 0; */
/*@ invariant this.last.next.priority % this.first.next.priority == 0; */
/*@ invariant this.first.next.priority % this.last.prev.priority == 0; */
/*@ invariant this.last.prev.priority % this.first.next.priority == 0; */
/*@ invariant this.first.next.priority % this.last.priority == 0; */
/*@ invariant this.last.priority % this.first.next.priority == 0; */
/*@ invariant this.first.val < this.last.next.val; */
/*@ invariant this.first.val <= this.last.prev.val; */
/*@ invariant this.first.val <= this.last.val; */
/*@ invariant this.first.priority % this.last.next.priority == 0; */
/*@ invariant this.last.next.priority % this.first.priority == 0; */
/*@ invariant this.first.priority % this.last.prev.priority == 0; */
/*@ invariant this.last.prev.priority % this.first.priority == 0; */
/*@ invariant this.first.priority % this.last.priority == 0; */
/*@ invariant this.last.priority % this.first.priority == 0; */
/*@ invariant this.last.next.val > this.last.prev.val; */
/*@ invariant this.last.next.val > this.last.val; */
/*@ invariant this.last.next.val >= this.memCount; */
/*@ invariant this.last.next.priority % this.last.prev.priority == 0; */
/*@ invariant this.last.prev.priority % this.last.next.priority == 0; */
/*@ invariant this.last.next.priority % this.last.priority == 0; */
/*@ invariant this.last.priority % this.last.next.priority == 0; */
/*@ invariant this.last.prev.val < this.last.val; */
/*@ invariant this.last.prev.priority % this.last.priority == 0; */
/*@ invariant this.last.priority % this.last.prev.priority == 0; */
Daikon refined invariant
Below are listed the properties that were maintained after manual inspection. Also, for each property we added validation in the case that some reference is null. For example, the property /*@ invariant this.curProc.prev == null; */ was rewritten as:
boolean isOK;
if (this.curProc!=null) {
isOK = this.curProc.prev == null;
}
Class Schedule
/*@ invariant this.MAXPRIO == this.prioQueue.length-1; */
/*@ invariant this.curProc.prev == null; */
/*@ invariant this.curProc.priority == 1 || this.curProc.priority == 2 || this.curProc.priority == 3; */
/*@ invariant this.prioQueue[this.curProc.priority] != null; */
/*@ invariant !(\forall int i; (0 <= i && i <= this.prioQueue.length-1) ==> (this.prioQueue[i] != this.blockQueue)); */
Class Job
/*@ invariant this.next == this.next.next.prev; */
/*@ invariant this.next == this.next.prev.next; */
/*@ invariant this.next == this.prev.next.next; */
/*@ invariant this.next.priority == this.priority; */
/*@ invariant this.prev.priority == this.priority; */
/*@ invariant this.val >= 0; */
/*@ invariant this.priority >= 0; */
Class List
/*@ invariant this.first.next.priority == this.first.priority; */
/*@ invariant this.first.next.priority == this.last.priority; */
/*@ invariant this.first.priority == this.last.next.priority; */
/*@ invariant this.first.priority == this.last.prev.priority; */
/*@ invariant this.first.priority == this.last.priority; */
/*@ invariant this.memCount >= 0; */