{size:int, n:nat, i:nat | n <= size, i < size}
unit heapify (heap[size]: float, n:int(n), i:int(i)) {
 var: int size, left, right;
      float temp;
      largest: [a:nat | a < size] int(a) ;;

 left = 2 * i + 1; right = 2 * i + 2;

 largest = i;

 if (left < n) {
   if (heap[left] >. heap[i]) { largest = left; }
 }

 if (right < n) {
   if (heap[right] >. heap[largest]) { largest = right; }
 }

 if (largest <> i) {
   temp = heap[i]; heap[i] = heap[largest]; heap[largest] = temp;
   heapify (heap, n, largest);
 }
}

{size:nat}
unit buildheap (n: int(size), heap[size]: float) {
 var: int i;;
 
 invariant: [i:int | i < size] (i: int(i))
 for (i = n / 2 - 1; i >= 0; i = i - 1) {
   heapify (heap, n, i);
 }
}

{size:nat}
unit heapsort (n: int(size), heap[size]: float) {
 var: int i; float temp;;

  buildheap (n, heap);
  invariant: [i:int | i < size] (i: int(i))
  for (i = n - 1; i >= 1; i = i - 1) {
    temp = heap[i]; heap[i] = heap[0]; heap[0] = temp;
    heapify(heap, i, 0);
  }
}