#include "arrays.pi"

define int ix = ?;

typedef struct qs {
  int pivot;
  int[] array;
} qs;

@pre  true
@post sorted(rv, 0, length(rv) - 1)
int[] QuickSort(int[] a)
{
  return qsort(a, 0, length(a) - 1);
}

@pre  0 <= l && u < length(a)
      && partitioned(a, 0, l - 1, l, u)
      && partitioned(a, l, u, u + 1, length(a) - 1) 
@post sorted(rv, l, u)
      && length(rv) == length(a)
      && eq(rv, a, 0, l - 1)
      && eq(rv, a, u + 1, length(a) - 1)
      && partitioned(rv, 0, l - 1, l, u)
      && partitioned(rv, l, u, u + 1, length(a) - 1) 
int[] qsort(int[] a, int l, int u)
declare
  qs p;
{
  if (l >= u) 
    return a;
  else {
    p = partition(a, l, u);
    a = p.array;
    a = qsort(a, l, p.pivot - 1);
    a = qsort(a, p.pivot + 1, u);
    return a;
  }
}

@pre  0 <= l && l <= u && u < length(a)
      && partitioned(a, 0, l - 1, l, u)
      && partitioned(a, l, u, u + 1, length(a) - 1) 
@post l <= rv.pivot && rv.pivot <= u
      && length(rv.array) == length(a)
      && partitioned(rv.array, l, rv.pivot - 1, rv.pivot, rv.pivot)
      && partitioned(rv.array, rv.pivot, rv.pivot, rv.pivot + 1, u)
      && eq(rv.array, a, 0, l - 1)
      && eq(rv.array, a, u + 1, length(a) - 1)
      && partitioned(rv.array, 0, l - 1, l, u)
      && partitioned(rv.array, l, u, u + 1, length(a) - 1) 
qs partition(int[] a, int l, int u)
declare
  int pi, pv, i, j, t;
  qs tmp;
{
  pi = random(l, u);
  pv = a[pi];
  a[pi] = a[u];
  a[u] = pv;

  i = l - 1;
  for
    @ true
    (j = l; j < u; j = j + 1)
  {
    if (a[j] <= pv) {
      i = i + 1;
      t = a[i];
      a[i] = a[j];
      a[j] = t;
    }
  }

  t = a[i + 1];
  a[i + 1] = a[u];
  a[u] = t;

  tmp.pivot = i + 1;
  tmp.array = a;
  return tmp;
}

@pre  l <= u
@post l <= rv && rv <= u
int random(int l, int u)
{
  /* a placeholder: only the @post is important */
  return u;
}