LARA

public /*: claimedby PriorityQueue */ class PriorityQueueElement {
    public Object ob;
    public int key;
}
 
public class PriorityQueue
{
    private PriorityQueueElement[] queue;
    private int length;
 
    /*:
      public specvar init :: bool = "False";
      public specvar content :: "(obj * int) set";
      public specvar smaxlen :: int;
      public specvar slength :: int;
 
      specvar spqueue :: "obj set";
 
      vardefs "init == (queue \<noteq> null)";
      vardefs "spqueue == {p. \<exists> i. 0 \<le> i \<and> i < length \<and> p = queue.[i]}";		   
      vardefs "content == {(x, y). EX p. p : spqueue & p..ob = x & p..key = y}";
      vardefs "smaxlen == queue..Array.length";
      vardefs "slength == length";
 
      invariant LengthLowerInv: "init \<longrightarrow> 0 \<le> length";
      invariant LengthUpperInv: "init \<longrightarrow> length \<le> queue..Array.length";
      invariant NonNullInv: "init \<longrightarrow> (\<forall> i. 0 \<le> i \<and> i < length \<longrightarrow> queue.[i] \<noteq> null)";
      invariant NullInv: 
       "init \<longrightarrow> (\<forall> i. length \<le> i \<and> i < queue..Array.length \<longrightarrow> queue.[i] = null)";
      invariant DistinctInv: "init \<longrightarrow> (\<forall> i j. 
        (0 \<le> i \<and> i < length \<and> 0 \<le> j \<and> j < length \<and> queue.[i] = queue.[j]) \<longrightarrow> i = j)"
      invariant OrderedInv: "init \<longrightarrow> (\<forall> i j.
       (0 \<le> i \<and> i < length \<and> 0 \<le> j \<and> j < length \<and> (j=i+i+1 \<or> j=i+i+2)
         \<longrightarrow> queue.[i]..key \<ge> queue.[j]..key))";
      invariant HiddenInv: "init \<longrightarrow> queue : hidden";
      invariant InjInv: "\<forall> x y. x..queue = y..queue \<and> x..queue \<noteq> null \<longrightarrow> x = y";
 
      invariant ContentInj: 
      "ALL e1 e2. e1 : spqueue & e2 : spqueue & e1 ~= e2 --> (e1..ob ~= e2..ob | e1..key ~= e2..key)";
 
    */
 
    public void PriorityQueue(int len)
    /*: requires "\<not>init \<and> 0 \<le> len"
        modifies init, content, smaxlen, slength
	ensures "init \<and> content = {} \<and> smaxlen = len \<and> slength = 0"
    */
    {
	queue = new /*: hidden */ PriorityQueueElement[len];
 
	int i = 0;
 
	while /*: inv "(\<forall> j. 0 \<le> j \<and> j < i \<longrightarrow> queue.[i] = null) \<and>
                       (\<forall> a i. a ~= queue \<longrightarrow> a.[i] = old (a.[i]))" */
	    (i < queue.length) {
	    queue[i] = null;
	}
	length = 0;
    }
 
    public int currLength()
    /*: requires "init"
        ensures "result = slength"
    */
    {
	return length;
    }
 
    public int maxLength()
    /*: requires "init"
        ensures "result = smaxlen"
    */
    {
	return queue.length;
    }
 
    public boolean isEmpty()
    /*: requires "init"
        ensures "result = (slength = 0)"
    */
    {
	return (length == 0);
    }
 
    public boolean isFull()
    /*: requires "init"
        ensures "result = (slength = smaxlen)"
    */
    {
	return (length == queue.length);
    }
 
    private static int parent(int i)
    /*: requires "i > 0"
        ensures "result >= 0 & result < i & 
	         (i = result + result + 1 | i = result + result +2) &
		 alloc = old alloc"
     */
    {
	return (i-1)/2;
    }
 
    private static int left(int i)
    /*: requires "0 \<le> i"
        ensures "0 \<le> result \<and> i < result \<and> result = 2 * i + 1 \<and> alloc = old alloc"
     */
    {
	return (2*i + 1);
    }
 
    private static int right(int i)
    /*: requires "0 \<le> i"
        ensures "0 \<le> result \<and> i < result \<and> result = 2 * i + 2 \<and> alloc = old alloc"
     */
    {
	return (2*i + 2);
    }
 
    public void insert(Object o1, int k1)
    /*: requires "init & o1 ~= null & slength < smaxlen & (o1, k1) ~: content"
        modifies content, slength
	ensures "content = old content Un {(o1, k1)} &
                 (slength = (old slength) + 1)"
    */
    {
	int i = length;
	length = length + 1;
 
	PriorityQueueElement e = new PriorityQueueElement();
	e.ob = o1;
	e.key = k1;
 
	while /*: inv "(comment ''IBounds'' (0 \<le> i \<and> i < length)) & 
		       e ~: spqueue &
		       alloc = old alloc Un {e} &
		       (comment ''RelToI''
		        (((i + i + 1 < length) -->
			  (queue.[(i + i + 1)]..PriorityQueueElement.key <
			   e..PriorityQueueElement.key)) &
			 ((i + i + 2 < length) -->
			  (queue.[(i + i + 2)]..PriorityQueueElement.key <
			   e..PriorityQueueElement.key)))) &
		       (comment ''ContentPostLoop''
		       (old spqueue = { p. EX j. 0 <= j & j < length &
                                          j ~= i & p = queue.[j] })) &
		       (ALL j. 0 <= j & j < length & j ~= i --> 
		               queue.[j] ~= null) & 
		       (comment ''PDBefore''
		        (ALL j k. 0 <= j & j < length & 0 <= k & k < length &
		                 queue.[j] = queue.[k] & j ~= i & k ~= i --> 
				 j = k)) &
		       theinv NullInv &
		       (comment ''OrderedSkipLoop''
		       (i = (old length) -->
		        (ALL j k. 
			 (0 <= j & j < (old length) & 0 <= k & 
			  k < (old length) &
			  ((k = j + j + 1) | (k = j + j + 2)) -->
			   queue.[j]..PriorityQueueElement.key >=
			   queue.[k]..PriorityQueueElement.key)))) &
		       (comment ''OrderedPostLoop''
		       (i ~= (old length) -->
		        (ALL j k. 
		         (0 <= j & j < length & 0 <= k & k < length &
			  ((k = j + j + 1) | (k = j + j + 2)) -->
			   queue.[j]..PriorityQueueElement.key >=
			   queue.[k]..PriorityQueueElement.key)))) \<and>
                       (\<forall> a i. a ~= queue \<longrightarrow> a.[i] = old (a.[i])) \<and>
                       (comment ''OrderedFrame'' 
                       (\<forall> pq. pq : PriorityQueue \<and> pq : alloc \<and> pq..init \<and> 
                        pq \<noteq> this \<longrightarrow> (\<forall> i j. 0 \<le> i \<and> i < pq..length \<and> 0 \<le> j \<and> 
                        j < pq..length \<and> (j = i + i + 1 \<or> j = i + i + 2) \<longrightarrow> 
                        pq..queue.[i]..key \<ge> pq..queue.[j]..key)))"
	      */
	    (i > 0 && queue[parent(i)].key < e.key)
	{
	    int p = parent(i);
 
	    //: noteThat PBounds: "0 \<le> p \<and> p < old length";
	    //: noteThat PIRel: "i = p + p + 1 | i = p + p + 2";
	    //: note InLoop: "queue.[p]..key < e..key";
 
	    queue[i] = queue[p];
 
	    /*: note iEffect1: "ALL jj. (0 \<le> jj \<and> jj < length \<and> 
	        ((i = jj + jj + 1) | (i = jj + jj + 2)) \<longrightarrow> 
	        queue.[jj]..key \<ge> queue.[i]..key)"; */
 
	    /*: note iEffect2: "ALL kk. (0 \<le> kk \<and> kk < length \<and>
	        ((kk = i + i + 1) | (kk = i + i + 2)) \<longrightarrow>
	        queue.[i]..key \<ge> queue.[kk]..key)" 
	        from OrderedPostLoop, InLoop, PIRel, PBounds; */
 
	    /*: note OtherEffect: 
	      "ALL jj kk. (0 \<le> jj \<and> jj < length \<and> 0 \<le> kk \<and> kk < length \<and> 
	       jj \<noteq> i \<and> kk \<noteq> i \<and> ((kk = jj + jj + 1) | (kk = jj + jj + 2)) \<longrightarrow> 
	       queue.[jj]..key \<ge> queue.[kk]..key)"; */
 
	    i = p;
 
	    /*: noteThat sameAfter:
	      "ALL jj kk. (0 <= jj & jj < length & 0 <= kk & kk < length & 
	      ((kk = jj + jj + 1) | (kk = jj + jj + 2)) -->
	      queue.[jj]..PriorityQueueElement.key >=
	      queue.[kk]..PriorityQueueElement.key)" 
	      from iEffect1, iEffect2, OtherEffect; */
 
	    /*: noteThat ContentAfter:
	      "old spqueue = 
	       { p. EX j. 0 <= j & j < length & j ~= i & p = queue.[j] }"
	      from ContentPostLoop, IBounds, PBounds;
	    */
	    /*: noteThat PDAfter:
	      "(ALL j k. 0 <= j & j < length & 0 <= k & k < length &
	                 queue.[j] = queue.[k] & j ~= i & k ~= i --> j = k)"
	      from PDBefore, PBounds;
	    */
	}
	queue[i] = e;
	/*: noteThat ContentDef:
	  "spqueue = {p. (EX i. 0 <= i & i < length & p = queue.[i])}";
	*/
	/*: noteThat NewSpqueue: "spqueue = old spqueue Un { e }"
	  from ContentPostLoop, ContentDef, IBounds;
	*/
 
	//: note ContentForw: "ALL x y. (x, y) : content --> (x, y) : old content Un {(o1, k1)}" from content_def, Hyp, NewSpqueue;
	{
	    //: pickAny x::obj, y::int;
	    {
		//: assuming Hyp: "(x, y) : old content Un {(o1, k1)}";
		{
		    //: assuming Hyp1: "(x, y) : old content";
		    //: note ENotInOld: "e ~: old spqueue";
		    //: note Conc1: "(x, y) : content" from content_def, ContentDef, NewSpqueue, Hyp1, ENotInOld;
		}
		//: note NewElemInContent: "(o1, k1) : content";
		//: note Conc: "(x, y) : content" from NewElemInContent, Conc1, Hyp;
	    }
	    //: note ContentBack: "(x, y) : old content Un {(o1, k1)} --> (x, y) : content" forSuch x, y;
	}
	//: note ContentPost: "content = old content Un {(o1, k1)}" from ContentForw, ContentBack;
 
	{
	    //: pickAny pq::obj;
	    {
		//: assuming ContentHyp: "pq : alloc & pq : PriorityQueue";
		{
		    //: pickAny e1::obj, e2::obj;
		    {
			//: assuming Hyp: "e1 : spqueue & e2 : spqueue & e1 ~= e2"
			{
			    //: assuming OldEs: "e1 : old spqueue & e2 : old spqueue";
			    //: note Conc1: "e1..ob ~= e2..ob | e1..key ~= e2..key";
			}
			{
			    //: assuming NewE1: "e1 ~: old spqueue";
			    //: note NewEntry: "(o1, k1) ~: old content";
			    //: note Conc2: "e1..ob ~= e2..ob | e1..key ~= e2..key" from Hyp, NewE1, content_def, NewSpqueue, NewEntry;
			}
			{
			    //: assuming NewE2: "e2 ~: old spqueue";
			    //: note NewEntry: "(o1, k1) ~: old content";
			    //: note Conc3: "e1..ob ~= e2..ob | e1..key ~= e2..key" from Hyp, NewE2, content_def, NewSpqueue, NewEntry;
			}
			//: note Conc: "e1..ob ~= e2..ob | e1..key ~= e2..key" from Conc1, Conc2, Conc3;
		    }
		    //: note ContentThis: "e1 : spqueue & e2 : spqueue & e1 ~= e2 --> (e1..ob ~= e2..ob | e1..key ~= e2..key)" forSuch e1, e2;
		}
		{
		    //: assuming NotThisHyp: "pq ~= this";
		    {
			//: pickAny e1::obj, e2::obj;
			{
			    //: assuming Hyp1: "e1 : pq..spqueue & e2 : pq..spqueue & e1 ~= e2";
			    //: note PQInOldAlloc: "pq : old alloc";
			    //: note ObKeyFrame: "e1 ~= e & e2 ~= e";
			    //: note OldContentInj: "e1 : fieldRead (old PriorityQueue.spqueue) pq & e2 : fieldRead (old PriorityQueue.spqueue) pq & e1 ~= e2 --> (e1..ob ~= e2..ob | e1..key ~= e2..key)" from ContentInj,  ContentHyp, PQInOldAlloc, ObKeyFrame;
			    //: note SpqueueFrame: "pq..spqueue = fieldRead (old PriorityQueue.spqueue) pq";
			    //: note Conc1: "(e1..ob ~= e2..ob | e1..key ~= e2..key)" from Hyp1, OldContentInj, SpqueueFrame, ObKeyFrame;
			}
			//: note NotThisConc: "e1 : pq..spqueue & e2 : pq..spqueue & e1 ~= e2 --> (e1..ob ~= e2..ob | e1..key ~= e2..key)" forSuch e1, e2;
		    }
		    //: note NotThisConc: "ALL e1 e2. e1 : pq..spqueue & e2 : pq..spqueue & e1 ~= e2 --> (e1..ob ~= e2..ob | e1..key ~= e2..key)";
		}
		//: note ContentInjConc: "ALL e1 e2. e1 : pq..spqueue & e2 : pq..spqueue & e1 ~= e2 --> (e1..ob ~= e2..ob | e1..key ~= e2..key)" from ContentThis, NotThisConc;
	    }
	    //: note ContentInjPost: "pq : alloc & pq : PriorityQueue --> (ALL e1 e2. e1 : pq..spqueue & e2 : pq..spqueue & e1 ~= e2 --> (e1..ob ~= e2..ob | e1..key ~= e2..key))" forSuch pq;
	}
	{
	    //: pickAny pq::obj;
	    {
		//: assuming Hyp: "pq : old alloc & pq : PriorityQueue & pq ~: hidden & pq ~= this";
		//: note ConcForw: "ALL x y. (x, y) : pq..content --> (x, y) : (fieldRead (old PriorityQueue.content) pq)";
		//: note ConcBack: "ALL x y. (x, y) : (fieldRead (old PriorityQueue.content) pq) --> (x, y) : pq..content";
		//: note ContentFrameConc: "pq..content = (fieldRead (old PriorityQueue.content) pq)" from ConcForw, ConcBack;
	    }
	    //: note ContentFrame: "pq : old alloc & pq : PriorityQueue & pq ~: hidden & pq ~= this --> pq..content = (fieldRead (old PriorityQueue.content) pq)" forSuch pq;
	}
    }
 
    public Object findMax()
    /*: requires "init \<and> slength > 0"
        ensures "(EX pr. (result, pr) \<in> content \<and>
	         (\<forall> x y. (x, y) \<in> content \<longrightarrow> pr \<ge> y))" */
    {
	{
	    //: assuming OrderingHyp1: "ALL i j. 0 <= i & i < length & 0 <= j & j < length & (j = i + i + 1 | j = i + i + 2) --> queue.[i]..key >= queue.[j]..key";
	    {
		//: pickAny k::int;
		{
		    //: assuming OrderingHyp2: "0 <= k & k < length";
		    //: note ArrLength: "0 < length";
		    {
			//: induct InGeneral: "ALL x. x <= kk & 0 <= x & x < length --> queue.[0]..key >= queue.[x]..key" over kk::int;
			//: note BaseCase: "ALL x. x <= 0 & 0 <= x & x < length --> queue.[0]..key >= queue.[x]..key";
			{
			    //: assuming InductHyp1: "ALL x. x <= kk & 0 <= x & x < length --> queue.[0]..key >= queue.[x]..key";
			    {
				//: pickAny x::int;
				{
				    //: assuming InductHyp2: "x <= (kk + 1) & 0 <= x & x < length";
				    {
					//: assuming LtHyp: "x < kk + 1";
					//: note LtConc: "queue.[0]..key >= queue.[x]..key";
				    }
				    {
					//: assuming EqHyp: "x = kk + 1";
					{
					    //: assuming EvenHyp: "x mod 2 = 0";
					    //: note EvenParent: "EX y. y + y = x" from EvenHyp;
					    {
						//: pickWitness evenp::int suchThat ParentRel: "evenp + evenp = x";
						//: note ParentGE: "queue.[evenp - 1]..key >= queue.[x]..key" from OrderingHyp1, EqHyp, ParentRel, OrderingHyp2, InGeneral, InductHyp2;
						//: note ParentInduct: "queue.[0]..key >= queue.[evenp - 1]..key" from InductHyp1, InductHyp2, EqHyp, ParentRel, InGeneral;
						//: note EvenPConc: "queue.[0]..key >= queue.[x]..key" from ParentInduct, ParentGE;
					    }
					    //: note EvenConc: "queue.[0]..key >= queue.[x]..key";
					}
					{
					    //: assuming OddHyp: "x mod 2 = 1";
					    //: note OddParent: "EX y. y + y + 1 = x" from OddHyp;
					    {
						//: pickWitness oddp::int suchThat ParentRel: "oddp + oddp + 1 = x";
						//: note ParentGE: "queue.[oddp]..key >= queue.[x]..key" from OrderingHyp1, ParentRel, InductHyp2;
						//: note ParentInduct: "queue.[0]..key >= queue.[oddp]..key" from InductHyp1, InductHyp2, EqHyp, ParentRel;
						//: note OddPConc: "queue.[0]..key >= queue.[x]..key" from ParentInduct, ParentGE;
					    }
					    //: note OddConc: "queue.[0]..key >= queue.[x]..key";
 
					}
					//: note EqConc: "queue.[0]..key >= queue.[x]..key" from EvenConc, OddConc;
 
				    }
				    //: note InductConc3: "queue.[0]..key >= queue.[x]..key" from LtConc, EqConc, InductHyp2;
				}
				//: note InductConc2: "x <= (kk + 1) & 0 <= x & x < length --> queue.[0]..key >= queue.[x]..key" forSuch x;
			    }
			    //: note InductConc1: "ALL x. x <= (kk + 1) & 0 <= x & x < length --> queue.[0]..key >= queue.[x]..key";
			}
		    }
		    //: note OrderingConc2: "queue.[0]..key >= queue.[k]..key" from InGeneral, ArrLength, OrderingHyp2;
		}
		//: note OrderingAll: "0 <= k & k < length --> queue.[0]..key >= queue.[k]..key" forSuch k;
	    }
	    //: note OrderingConc1: "ALL k. 0 <= k & k < length --> queue.[0]..key >= queue.[k]..key";
	}
	//: note QueueDef: "spqueue = {p. EX i. 0 <= i & i < length & p = queue.[i]}";
	//: note LengthLemma: "0 < length";
	//: note FoundElem: "queue.[0] : spqueue" from QueueDef, LengthLemma;
	//: note FoundPair: "(queue.[0]..ob, queue.[0]..key) : content";
	//: note IsMax: "ALL x y. (x, y) : content --> queue.[0]..key >= y";
	return queue[0].ob;
    }
 
    public Object extractMax()
    /*: requires "init \<and> slength > 0"
        modifies content, slength
        ensures  "slength = old slength - 1 \<and> 
	          (EX pr. content = old content - { (result, pr) } \<and>
		  (\<forall> x y. (x, y) \<in> (old content) \<longrightarrow> pr \<ge> y))" */
    {
	PriorityQueueElement result = queue[0];
	{
	    //: assuming OrderingHyp1: "ALL i j. 0 <= i & i < length & 0 <= j & j < length & (j = i + i + 1 | j = i + i + 2) --> queue.[i]..key >= queue.[j]..key";
	    {
		//: pickAny k::int;
		{
		    //: assuming OrderingHyp2: "0 <= k & k < length";
		    //: note ArrLength: "0 < length";
		    {
			//: induct InGeneral: "ALL x. x <= kk & 0 <= x & x < length --> queue.[0]..key >= queue.[x]..key" over kk::int;
			//: note BaseCase: "ALL x. x <= 0 & 0 <= x & x < length --> queue.[0]..key >= queue.[x]..key";
			{
			    //: assuming InductHyp1: "ALL x. x <= kk & 0 <= x & x < length --> queue.[0]..key >= queue.[x]..key";
			    {
				//: pickAny x::int;
				{
				    //: assuming InductHyp2: "x <= (kk + 1) & 0 <= x & x < length";
				    {
					//: assuming LtHyp: "x < kk + 1";
					//: note LtConc: "queue.[0]..key >= queue.[x]..key";
				    }
				    {
					//: assuming EqHyp: "x = kk + 1";
					{
					    //: assuming EvenHyp: "x mod 2 = 0";
					    //: note EvenParent: "EX y. y + y = x" from EvenHyp;
					    {
						//: pickWitness evenp::int suchThat ParentRel: "evenp + evenp = x";
						//: note ParentGE: "queue.[evenp - 1]..key >= queue.[x]..key" from OrderingHyp1, EqHyp, ParentRel, OrderingHyp2, InGeneral, InductHyp2;
						//: note ParentInduct: "queue.[0]..key >= queue.[evenp - 1]..key" from InductHyp1, InductHyp2, EqHyp, ParentRel, InGeneral;
						//: note EvenPConc: "queue.[0]..key >= queue.[x]..key" from ParentInduct, ParentGE;
					    }
					    //: note EvenConc: "queue.[0]..key >= queue.[x]..key";
					}
					{
					    //: assuming OddHyp: "x mod 2 = 1";
					    //: note OddParent: "EX y. y + y + 1 = x" from OddHyp;
					    {
						//: pickWitness oddp::int suchThat ParentRel: "oddp + oddp + 1 = x";
						//: note ParentGE: "queue.[oddp]..key >= queue.[x]..key" from OrderingHyp1, ParentRel, InductHyp2;
						//: note ParentInduct: "queue.[0]..key >= queue.[oddp]..key" from InductHyp1, InductHyp2, EqHyp, ParentRel;
						//: note OddPConc: "queue.[0]..key >= queue.[x]..key" from ParentInduct, ParentGE;
					    }
					    //: note OddConc: "queue.[0]..key >= queue.[x]..key";
 
					}
					//: note EqConc: "queue.[0]..key >= queue.[x]..key" from EvenConc, OddConc;
 
				    }
				    //: note InductConc3: "queue.[0]..key >= queue.[x]..key" from LtConc, EqConc, InductHyp2;
				}
				//: note InductConc2: "x <= (kk + 1) & 0 <= x & x < length --> queue.[0]..key >= queue.[x]..key" forSuch x;
			    }
			    //: note InductConc1: "ALL x. x <= (kk + 1) & 0 <= x & x < length --> queue.[0]..key >= queue.[x]..key";
			}
		    }
		    //: note OrderingConc2: "queue.[0]..key >= queue.[k]..key" from InGeneral, ArrLength, OrderingHyp2;
		}
		//: note OrderingAll: "0 <= k & k < length --> queue.[0]..key >= queue.[k]..key" forSuch k;
	    }
	    //: note OrderingConc1: "ALL k. 0 <= k & k < length --> queue.[0]..key >= queue.[k]..key";
	}
	length = length - 1;
	queue[0] = queue[length];
	queue[length] = null;
	//: noteThat IntQueueContent: "spqueue = old spqueue - { result }";
	if (0 < length) heapify(0);
	/*: noteThat FinalQueueContent: "spqueue = old spqueue - { result }"
	  from IntQueueContent, heapify_Postcond, FinalQueueContent; */
 
	{
	    //: pickAny x1::obj, y1::int;
	    {
		//: assuming RemovedForwHyp: "(x1, y1) : content";
		//: note ResultInOld: "result : old spqueue";
		//: note ContentInjLemma: "ALL e1 e2. e1 : old spqueue & e2 : old spqueue & e1 ~= e2 --> (e1..ob ~= e2..ob | e1..key ~= e2..key)";
		//: note RemovedForwConc: "(x1, y1) : old content - {(result..ob, result..key)}" from Hyp, ContentInjLemma, content_def, FinalQueueContent, ResultInOld;
	    }
	    //: note RemovedForw: "(x1, y1) : content --> (x1, y1) : old content - {(result..ob, result..key)}" forSuch x1, y1;
	}
	{
	    //: pickAny x2::obj, y2::int;
	    {
		//: assuming RemovedBackHyp: "(x2, y2) : old content - {(result..ob, result..key)}";
		//: note RemovedBackConc: "(x2, y2) : content" from content_def, RemovedBackHyp, FinalQueueContent;
	    }
	    //: note RemovedBack: "(x2, y2) : old content - {(result..ob, result..key)} --> (x2, y2) : content" forSuch x2, y2;
	}
	//: note RemovedPair: "content = old content - {(result..ob, result..key)}" from RemovedForw, RemovedBack;
	//: note IsMax: "ALL x y. (x, y) : old content --> result..key >= y";
	/*: witness "result..key" for
	  PostCond: "EX pr. content = old content - {(result..ob, pr)} & (ALL x y. (x, y) : (old content) --> pr >= y)"
	  from RemovedPair, IsMax; */
 
	{
	    //: pickAny pq::obj;
	    {
		//: assuming Hyp: "pq : old alloc & pq : PriorityQueue & pq ~: hidden & pq ~= this";
		//: note ConcForw: "ALL x y. (x, y) : pq..content --> (x, y) : (fieldRead (old PriorityQueue.content) pq)";
		//: note ConcBack: "ALL x y. (x, y) : (fieldRead (old PriorityQueue.content) pq) --> (x, y) : pq..content";
		//: note ContentFrameConc: "pq..content = (fieldRead (old PriorityQueue.content) pq)" from ConcForw, ConcBack;
	    }
	    //: note ContentFrame: "pq : old alloc & pq : PriorityQueue & pq ~: hidden & pq ~= this --> pq..content = (fieldRead (old PriorityQueue.content) pq)" forSuch pq;
	}
	return result.ob;
    }
 
    private void heapify(int i)
    /*: requires "init \<and> 0 \<le> i \<and> i < length \<and> 
                  theinv LengthLowerInv \<and>
                  theinv LengthUpperInv \<and> theinv NonNullInv \<and>
		  theinv NullInv \<and> theinv DistinctInv \<and>
		  (comment ''GlobalOrderingPre''
		   (ALL k j.
		    (0 <= k & k < length & k ~= i & 0 < j & j < length &
		    ((j = k + k + 1) | (j = k + k + 2)) -->
		    queue.[k]..PriorityQueueElement.key >=
		    queue.[j]..PriorityQueueElement.key))) \<and> 
		  (comment ''LocalOrderingPre''
		   (ALL x. 
		    ((0 <= x & (i = x + x + 1 | i = x + x + 2)) -->
		     (((i + i + 1 < length) --> 
		      queue.[x]..PriorityQueueElement.key >=
		      queue.[(i + i + 1)]..PriorityQueueElement.key) &
		      ((i + i + 2 < length) -->
		      queue.[x]..PriorityQueueElement.key >=
		      queue.[(i + i + 2)]..PriorityQueueElement.key))))) \<and> 
                  (comment ''OrderedFrame'' 
                   (\<forall> pq. pq : PriorityQueue \<and> pq : alloc \<and> 
		    pq..init \<and> pq \<noteq> this \<longrightarrow> 
	            (\<forall> i j. 0 \<le> i \<and> i < pq..length \<and> 
		     0 \<le> j \<and> j < pq..length \<and> 
	             (j = i + i + 1 \<or> j = i + i + 2) \<longrightarrow> 
	             pq..queue.[i]..key \<ge> pq..queue.[j]..key))) \<and>
	         theinv HiddenInv \<and> theinv InjInv \<and>
		 theinv ContentInj"
        modifies "Array.arrayState"
        ensures "(\<forall> pq. pq..init = old (pq..init)) \<and> 
	         (\<forall> pq. pq..spqueue = old (pq..spqueue)) \<and> 
	         (\<forall> pq. pq..smaxlen = old (pq..smaxlen)) \<and> 
	         (\<forall> pq. pq..slength = old (pq..slength)) \<and> 
	         alloc = old alloc \<and> theinvs \<and>
	         (\<forall> a i. a \<noteq> queue \<longrightarrow> 
		  a.[i] = old (a.[i]))" */
    {
	int m = i;
 
	int l = left(i);
	if (l < length && queue[l].key > queue[i].key)
	    m = l;
 
	int r = right(i);
	if (r < length && queue[r].key > queue[m].key)
	    m = r;
 
	if (m != i)
	{
	    PriorityQueueElement p = queue[m];
	    queue[m] = queue[i];
	    queue[i] = p;
	    /*: note ContentBefore: 
	        "\<forall> pq. pq..spqueue = old (pq..spqueue)"; */
	    heapify(m);
	    /*: note ContentAfter: 
	        "\<forall> pq. pq..spqueue = old (pq..spqueue)"
		from ContentBefore, heapify_Postcond; */
	    /*: note ContentFrame: 
		"\<forall> pq. pq \<in> PriorityQueue \<longrightarrow> 
		 pq..spqueue = old (pq..spqueue)"
		from ContentAfter; */
	}
    }
}