
#include "sort_heap.h"
#include "../pop_heap/pop_heap.h"
#include "LowerBound.h"
#include "SortedUpperBound.h"
#include "Unchanged.h"
#include "MultisetUnchangedLemmas.h"

void sort_heap(value_type* a, size_type n)
{
  /*@
     loop invariant bound:    0 <= i <= n;
     loop invariant heap:     IsHeap(a, i);
     loop invariant sorted:   Sorted(a, i, n);
     loop invariant lower:    LowerBound(a, i, n, a[0]);
     loop invariant reorder:  MultisetUnchanged{Pre,Here}(a, 0, n);
     loop assigns i, a[0..n-1];
     loop variant i;
  */
  for (size_type i = n; i > 1; --i) {
    //@ ghost Loop: ;
    //@ assert \true;
    /*@
        requires heap:     IsHeap(a, i);
        assigns  a[0..i-1];
        ensures  heap:     IsHeap(a, i-1);
        ensures  max:      a[i-1] == \old(a[0]);
        ensures  max:      MaxElement(a, i, i-1);
        ensures  reorder:  MultisetUnchanged{Old,Here}(a, 0, i);
        ensures  reorder:  Unchanged{Old,Here}(a, i, n);
    */
    pop_heap(a, i);
    //@ assert \true;
    //@ assert \true;
    //@ assert \true;
  }
}

