Representing queue using a Model Method import org.jmlspecs.models.JMLObjectBag; public class Heap implements PriorityQueue { private Comparable[] elems; private int numElems; private represents queue = computeQueue(); private model pure non_null JMLObjectBag computeQueue() { JMLObjectBag bag = new JMLObjectBag(); for (int i = 0; i < numElems; i++) { bag = bag.insert(elems[i]); } return bag;
{}