Heap2.java

File contents

abstract class HeapElem implements Comparable {
    // The position in the heap.
    /*@ spec_public @*/ int heapPos = -1;
}

class Heap2Solved {
    private /*@ spec_public @*/ HeapElem[] elems;
    private /*@ spec_public @*/ int numElems;

    public Heap2Solved() {
	elems = new HeapElem[5];
	numElems = 0;
    }

    /*@ public invariant (\forall int i; i >= 0 && i < numElems; 
      @                        elems[i] != null && 
      @			       elems[i].heapPos == i);
      @ public invariant 0 <= numElems && numElems <= elems.length;
      @ public invariant elems != null && elems.length > 0;
      @*/
      
    /*@ requires elems != null && elems.length > 0 && 
      @          0 <= numElems && numElems <= elems.length;
      @ ensures elems != null && elems.length > \old(elems.length)
      @       && numElems == \old(numElems)
      @       && (\forall int i; i >= 0 && i < numElems;
      @           elems[i] == \old(elems[i]));
      @ modifies elems;
      @*/
    private void grow() {
	HeapElem[] newElems = new HeapElem[elems.length*2];
	/*@ loop_invariant 0<= i && i <= elems.length;
	  @ loop_invariant (\forall int j; j >= 0 && j < i;
	  @           newElems[j] == \old(elems[j]));
	  @*/
	for (int i = 0; i < numElems; ++i)
	    newElems[i] = elems[i];
	elems = newElems;
    }

    /*@ requires e.heapPos == -1;
      @ ensures e.heapPos >= 0 && e.heapPos < numElems &&
      @         (Object) elems[e.heapPos] == (Object) e &&
      @         (\forall int i; i >= 0 && i < numElems; i == e.heapPos || 
      @                  (Object) elems[i] != (Object) e);
      @*/
    public void enqueue(HeapElem e) {
	if (numElems >= elems.length)
	    grow();
	//@ assert (\forall int i; i >= 0 && i < numElems; elems[i] != null && elems[i].heapPos == i);
	int pos = numElems++;
	int parent = pos / 2;
	/*@ loop_invariant (\forall int i; i >= 0 && i < numElems && i != pos; 
	  @                        elems[i] != null && elems[i] != e &&
	  @			       elems[i].heapPos == i);
	  @ loop_invariant 0 <=  pos && pos < numElems && parent == pos/2;
	  @*/
	while (pos > 0 && elems[parent].compareTo(e) > 0) {
	    elems[parent].heapPos = pos;
	    elems[pos] = elems[parent];
	    pos = parent;
	    parent = pos / 2;
	}
	elems[pos] = e;
	e.heapPos = pos;
    }
    
    /*@
      @ requires e.heapPos >= 0 && e.heapPos < numElems && 
      @          elems[e.heapPos] == e && numElems < 1000000000;
      @*/
    public void remove(HeapElem e) {
	HeapElem last = elems[--numElems];
	int pos = e.heapPos;
	e.heapPos = -1;
	if (last == e) {
	    return;
	}
	int child = 2*pos+1;
	/*@ loop_invariant (\forall int i; i >= 0 && i < numElems && i != pos; 
	  @                        elems[i] != null && elems[i] != last &&
	  @			       elems[i].heapPos == i);
	  @ loop_invariant 0 <=  pos && pos < numElems && child == 2*pos+1;
	  @*/
	while (child < numElems) {
	    if (child + 1 < numElems
		&& elems[child].compareTo(elems[child+1]) > 0) {
		child++;
	    }

	    if (elems[child].compareTo(last) > 0)
		break;

	    elems[pos] = elems[child];
	    elems[pos].heapPos = pos;
	    pos = child;
	    child = 2*pos+1;
	}
	elems[pos] = last;
	last.heapPos = pos;
    }
}