/* Rearranges the elements in the given array so that the ones
** in a[0..pivotLoc) are less than a[pivotLoc], and the elements
** in a[pivotLoc+1..a.Length) are >= a[pivotLoc].
** This implementation chooses the value in a[a.Length-1] to serve
** as the "pivot".
*/
method Partition(a: array<int>) returns (pivotLoc: nat)
   modifies a
   requires a.Length != 0
   ensures 0 <= pivotLoc < a.Length
   ensures forall i | 0 <= i < pivotLoc :: a[i] < a[pivotLoc]
   ensures forall i | pivotLoc <= i < a.Length :: a[pivotLoc] <= a[i]
   ensures multiset(a[..]) == old(multiset(a[..]))
{
   var left: nat := 0;
   var right: nat := a.Length - 1;
   // Variable 'pivotVal' serves only to avoid repeated references
   // to a[a.Length-1] and, as such, does not play a vital role here.
   var pivotVal := a[a.Length-1];
   while left != right
      decreases right - left
      invariant 0 <= left <= right < a.Length
      invariant pivotVal == a[a.Length-1]
      invariant forall i | 0 <= i < left :: a[i] < pivotVal
      invariant forall i | right <= i < a.Length :: pivotVal <= a[i]
      invariant multiset(a[..]) == old(multiset(a[..]))
   {
      if a[left] < pivotVal { left := left+ 1; }
      else if a[right-1] >= pivotVal { right := right - 1; }
      else {
         a[left], a[right-1] := a[right-1], a[left];
         left, right := left+1, right-1;
      }
   }
   // Finally, place the pivot value into its proper location, at the
   // border between values less than it and those not less than it. 
   a[left], a[a.Length-1] := pivotVal, a[left];
   pivotLoc := left;
}


// Yields true iff the values in each row of the given 2-dim array
// are in increasing order.
predicate increasingRowOrder(a: array2<int>)
   reads a
{
    forall i,j,j' | 0 <= i < a.Length0 && 0<=j<j'< a.Length1 :: a[i,j] < a[i,j']
}

// Yields true iff the values in each column of the given 2-dim array
// are in increasing order.
predicate increasingColOrder(a: array2<int>)
   reads a
{
    forall i,i',j | 0 <= i < i' < a.Length0 && 0<=j<a.Length1 :: a[i,j] < a[i',j]
}

// Yields true iff key occurs in a[].
predicate occursIn(a: array2<int>, key: int) 
   reads a
{
   exists i,j | 0<=i<a.Length0 && 0<=j<a.Length1 :: a[i,j] == key
}

/* Assuming that the given 'key' value occurs in the given
** 2-dim array (whose value increase across each row and each
** column), returns (m,n) such that a[m,n] == key.  
*/
method SlopeSearch(a: array2<int>, key: int) returns (m: nat, n: int)
   requires a.Length0 != 0
   requires a.Length1 != 0
   //requires occursIn(a,key)
   requires increasingRowOrder(a)
   requires increasingColOrder(a)
   ensures 0 <= m <= a.Length0
   ensures -1 <= n < a.Length1
   ensures occursIn(a,key) ==> 0<=m<a.Length0  && 0<=n<a.Length1 && a[m,n] == key
   ensures !occursIn(a,key) ==> m == a.Length0 || n == -1
{
   m := 0;
   n := a.Length1 - 1;
   while m != a.Length0 && n != -1 && a[m,n] != key
      decreases n + (a.Length0 - m)
      invariant 0 <= m <= a.Length0
      invariant -1 <= n < a.Length1
      // Next invariant says that if the key is in a[], then
      // it must be in that portion of a[] that has not yet
      // been explored, namely the rectangle whose "low corner"
      // is (m,0) and whose high corner is (a.Length0-1,n)
      invariant occursIn(a,key) ==> 
          exists i,j | m<=i<a.Length0 && 0<=j<=n :: a[i,j] == key
   {
      if a[m,n] < key { m := m+1; }
      else { n := n-1; }
   }
}