Heap1.java

File contents

import java.io.*;
import java.util.HashMap;

public class Heap1 {
    private /*@ spec_public @*/ /*@ rep rep @*/ HeapElem[] elems;
    private /*@ spec_public @*/ int numElems;

    public Heap1() {
	    elems = new /*@ rep rep @*/ HeapElem[5];
	    numElems = 0;
    }

    /*@ invariant (\forall int i; i >= 0 && i < numElems; 
				       elems[i].heapPos == i &&
				       (readonly Object) elems[i].owner == (readonly Object) this);
      @*/

    /*@ ensures elems.length > \old(elems.length)
      @       && numElems == \old(numElems);
      @*/
    private void grow() {
	/*@ rep rep @*/ HeapElem[] newElems = new /*@ rep rep @*/ HeapElem[elems.length*2];
	for (int i = 0; i < numElems; ++i)
	    newElems[i] = elems[i];
	elems = newElems;
    }

    /*@ requires e.heapPos == -1;
      @ ensures e.heapPos >= 0 && e.heapPos < numElems &&
      @         (readonly Object) elems[e.heapPos] == (readonly Object) e &&
      @         (\forall int i; i >= 0 && i < numElems; i == e.heapPos || 
      @                  (readonly Object) elems[i] != (readonly Object) e);
      @*/
    public void enqueue(/*@ rep @*/ HeapElem e) {
	if (numElems >= elems.length)
	    grow();
	int pos = numElems++;
	int 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;
    }

    public /*@ rep @*/ HeapElem getFirst() {
	return elems[0];
    }

    /*@
      @ requires e.heapPos >= 0 && e.heapPos < numElems && 
      @          (readonly Object) elems[e.heapPos] == (readonly Object) e;
      @ ensures (\forall int i; i >= 0 && i < numElems; 
      @                  (readonly Object) elems[i] != (readonly Object) e);
      @*/
    public void remove(/*@ rep @*/ HeapElem e) {
	/*@ rep @*/ HeapElem last = elems[--numElems];
	int pos = e.heapPos;
	e.heapPos = -1;
	if ((/*@ readonly @*/ Object) last == (/*@ readonly @*/ Object) e)
	    return;
	int child = 2*pos+1;
	elems[pos] = last;
	last.heapPos = pos;
	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;
    }

    public boolean isEmpty() {
	return numElems == 0;
    }
}

class User {
  public void test() {
	Heap1 h1 = new Heap1();
	IntHeapElem elem1 = new IntHeapElem(1);
	h1.enqueue(elem1);
	IntHeapElem elem2 = new IntHeapElem(2);
	h1.enqueue(elem2);

	HeapElem h1First = h1.getFirst();
	h1.remove(h1First);

	Heap1 h2 = new Heap1();
	h2.enqueue(h1First);
  }
}

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

class IntHeapElem extends HeapElem {
    int key;
    public IntHeapElem(int k) {
	key = k;
    }
    public int compareTo(Object other) {
	return key - ((IntHeapElem) other).key;
    }
    public /*@ pure @*/ boolean equals(/*@ nullable @*/ Object o) {
	if (o == null || !(o instanceof IntHeapElem))
	    return false;
	return key == ((IntHeapElem) o).key;
    }

    public /*@ pure @*/ String toString() {
	return "" + key;
    }
}