predicate sorted(a: array<int>)
 requires a != null;
 reads a;
{
  forall j,k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}

predicate sortedPart(a: array<int>, n : int)
 requires a != null;
 requires n <= a.Length;
 reads a;
{
  forall j,k :: 0 <= j < k < n ==> a[j] <= a[k]
}

lemma transitivelyOrdered(a: array<int>, n : int, i : int, j : int)
  requires a != null;
  requires n <= a.Length;
  requires forall i :: 0 <= i < n-1 ==> a[i] <= a[i+1];
  requires 0 <= i < j < n;
  decreases j - i;
  ensures a[i] <= a[j];
{
  if (j == i + 1) { }
  else { transitivelyOrdered(a, n, i+1, j); }
}

predicate pairwiseOrdered(a : array<int>, n : int)
  requires a != null;
  requires n <= a.Length;
  reads a;
{
  forall i :: 0 <= i < n-1 ==> a[i] <= a[i+1]
}

lemma pairwiseOrderedIsSorted(a : array<int>, n : int)
  requires a != null;
  requires n <= a.Length;
  requires pairwiseOrdered(a, n);
  ensures sortedPart(a, n);
{
  forall(i, j | 0 <= i < j < n) { transitivelyOrdered(a, n, i, j); }
}

method srt(a : array<int>)
 requires a != null;
 requires a.Length >= 1;
 modifies a;
 ensures sorted(a);
{
  var i := 0;
  while (i < a.Length-1)
    invariant i >= 0 && i < a.Length;
    invariant 0 < i ==> pairwiseOrdered(a, i+1);
    invariant forall e :: 0 < i < e < a.Length ==> a[i-1] <= a[e];
  {
    var j := i + 1;

    while (j < a.Length)
      invariant j <= a.Length;
      invariant forall e :: 0 <= i < e < j <= a.Length ==> a[i] <= a[e];
      invariant forall r :: 0 < i < r < a.Length ==> a[i-1] <= a[r];
      invariant pairwiseOrdered(a, i+1);
    {
      if (a[i] > a[j]) {
        a[i], a[j] := a[j], a[i];
      }
      j := j+1;
    }
    i := i+1;
  }
  pairwiseOrderedIsSorted(a, a.Length);
}

method srt1(a : array<int>)
  requires a != null;
  modifies a;
{
  var i := 0;
  while (i < a.Length-1)
  {
    var j := i + 1;

    while (j < a.Length)
    {
      if (a[i] > a[j]) {
        a[i], a[j] := a[j], a[i];
      }
      j := j+1;
    }
    i := i+1;
  }
}


method show(a : array<int>)
  requires a != null;
{
  var i := 0;
  while(i < a.Length) {
    print a[i], " ";
    i := i+1;
  }
  print "\n";
}

method binarySearch(a: array<int>, key:int) returns (i : int)
 requires a != null && sorted(a);
 ensures 0 <= i ==> i < a.Length && a[i]==key;
 ensures i < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key;
{
  var low, high := 0, a.Length;
  while(low < high)
    invariant 0 <= low <= high <= a.Length;
    invariant forall j :: 0 <= j < a.Length && !(low <= j < high) ==> a[j] != key;
  {
    var mid := (high + low) / 2;
    if (a[mid] < key) {
      low := mid +1;
    } else if (key < a[mid]) {
      high := mid;
    } else {
      i := mid; return;
    }
  }
  i := -1;
}

function method multisetOf<T>(a : array<T>, i : int) : multiset<T>
  requires a != null;
  requires 0 <= i <= a.Length;
  reads a;
  decreases a.Length - i;
{
  if i == a.Length then multiset{}
  else
  multisetOf(a, i+1) + multiset{a[i]}
}

function method elements<T>(a : array<T>) : multiset<T>
  requires a != null;
  reads a;
{
  multisetOf(a,0)
}

function method isPerm<T(==)>(a : array<T>, b : array<T>) : bool
  requires a != null && b != null;
  reads a, b;
{
  elements(a) == elements(b)
}

method test(a : array<int>)
  requires a != null && a.Length >= 2;
  modifies a;
  ensures isPerm(a, old(a));
{
  a[0], a[1] := a[1], a[0];
}

method Main()
{
  var a := new int[5];
  a[0] := 4;
  a[1] := 3;
  a[2] := 6;
  a[3] := 1;
  a[4] := 2;
  srt(a);
  show(a);
  var ms := elements(a);
  print ms;
  print isPerm(a,a);
  test(a);
  show(a);
  //var i := binarySearch(a, 3);
  //print i;
}