public class Quicksort {

  private static int partition(Node[] a, int i, int j, int key)
  /*:
    requires
      " a ~= null
      & 0 <= i & i <= j & j < Array.length a
      & (ALL k. (i <= k & k <= j) --> a.[k] ~= null)
      "
    modifies "Array.arrayState"
    ensures
      " i <= result
      & (ALL k. (i <= k & k <= j) --> a.[k] ~= null)
      & (ALL k. (i <= k & k <= j) --> (EX l. i <= l & l <= j & a.[k]=old(a.[l])))
      & (ALL k. (i <= k & k <= j & k < result) --> a.[k]..Node.key < key)
      & (ALL k. (result <= k & k <= j) --> key <= a.[k]..Node.key)
      & (ALL k. (k < i | j < k) --> a.[k]=old(a.[k]))
      "
   */
  {
      int l = i;
      int r = j;

      while
          /*: inv
            " i <= l & l <= j + 1
            & r <= j & (i - 1) <= r
            & (ALL k. (i <= k & k < l) --> a.[k]..Node.key < key)
            & (ALL k. (r < k & k <= j) --> key <= a.[k]..Node.key)
            & (ALL k. (i <= k & k <= j) --> a.[k] ~= null)
            & (ALL k. (i <= k & k <= j) --> (EX l. i <= l & l <= j & a.[k]=old(a.[l])))
            & (ALL k. (k < i | j < k) --> a.[k]=old(a.[k]))
            "
           */
          (l<=r)
      {
          while
              /*: inv
                " i <= l & l <= (j + 1)
                & (ALL k. (i <= k & k < l) --> a.[k]..Node.key < key)
                "
              */
              (l <= j && a[l].key < key)
          {
              l = l + 1;
          }
          
          while
              /*: inv
                " r <= j & (i - 1) <= r
                & (ALL k. (r < k & k <= j) --> key <= a.[k]..Node.key)
                "
              */
              (i <= r && key <= a[r].key)
          {
              r = r - 1;
          }
          
          if (l<=r) {
              Node t = a[l];
              a[l] = a[r];
              a[r] = t;
              l = l + 1;
              r = r - 1;
          }
      }

      return l;
  }

  private static void quicksort(Node[] a, int i, int j)
  /*:
    requires
      " a ~= null
      & 0 <= i
      & i <= j
      & j < Array.length a
      & (ALL k. (i <= k & k <= j) --> a.[k] ~= null)
      "
    modifies "Array.arrayState"
    ensures
      " (ALL k. (i <= k & k <= j) --> a.[k] ~= null)
      & (ALL k. (i <= k & k <= j) --> (EX l. i <= l & l <= j & a.[k]=old(a.[l])))
      & (ALL k. (k < i | j < k) --> a.[k] = old(a.[k]))
      & (ALL k. (i <= k & k < j) --> a.[k]..Node.key <= a.[k+1]..Node.key)
      "
   */
  {
      if (j==i) return;
      int key = a[i].key;
      //:assume "False"
      int k = partition(a, i, j, key);
      if (i <= k-1 && k-1 <= j) {
          quicksort(a, i, k-1);
      }
      if (i <= k && k <= j) {
          quicksort(a, k, j);
      }
  }

  public static void sort(Node[] a)
  /*:
    requires
      " a ~= null
      & (ALL k. (0 <= k & k < Array.length a) --> a.[k] ~= null)
      " 
    modifies "Array.arrayState"
    ensures
      " (ALL k. (0 <= k & k < Array.length a) --> a.[k] ~= null)
      & (ALL k. (0 <= k & k < Array.length a - 1) --> (a.[k]..Node.key <= a.[k+1]..Node.key))
      "
   */
  {
      if (a.length > 0) {
          //: assume "False"
          quicksort(a, 0, a.length-1);
      }
  }
}