predicate sorted(a: array<int>)
	reads a
{
	forall i ::  (0 <= i < a.Length - 1) ==> a[i] <= a[i + 1]
}

// If an array is not sorted, then find a pair of consecutive elements that witness the fact that it is not sorted.
// Recursive counterpart of violationVersion1 in circular-search-proof.dfy:
// same computation, same circular termination measure (Ruotong's Measure),
// expressed as recursion instead of a while loop.

method violation(a : array<int>) returns (i : nat)
  requires a.Length > 1
  requires !sorted(a)
  ensures 0 <= i < a.Length - 1
  ensures a[i] > a[i + 1]
{
    ghost var j :| 0 <= j < a.Length - 1 && a[j] > a[j + 1];

    var n := *;
    i := search(a, n % (a.Length - 1), j);
}

method search(a: array<int>, i: nat, ghost j: nat) returns (result: nat)
  requires a.Length > 1
  requires 0 <= i < a.Length - 1
  requires 0 <= j < a.Length - 1 && a[j] > a[j + 1]
  ensures 0 <= result < a.Length - 1
  ensures a[result] > a[result + 1]
  decreases if i <= j then j - i else a.Length + j - i 
  // Try the non-conditional measure and give the proof as an exercise
{
    if a[i] > a[i + 1] {
        result := i;
    } else {
        result := search(a, (i + 1) % (a.Length - 1), j);
    }
}