Verify This -- Challenge I: Lexicographic Permutations

next.dfy

lemma contains_implies_index (k : nat, perm : seq<nat>)
  requires k in perm
  ensures exists m :: 0 <= m < |perm| && perm[m] == k
{
}

method next (perm: array<nat>) returns (res: bool)
  modifies perm
  requires forall k :: 1 <= k <= perm.Length ==> k in perm[..]
  ensures !res ==> forall k :: 0 <= k < perm.Length ==> perm[k] == old(perm[k])
  ensures !res ==> forall k :: 0 <= k < perm.Length - 1 ==> perm[k] >= perm[k+1]
  ensures forall k :: 1 <= k <= perm.Length ==> k in perm[..]
{

  if perm.Length <= 0
  {
    return false;
  }
  var i : int := perm.Length - 1;
  while i > 0 && perm[i-1] >= perm[i]
    invariant i >= 0
    invariant forall k :: i < k <= perm.Length - 1 ==> perm[k-1] >= perm[k]
  {
    i := i - 1;
  }
  if i <= 0
  {
    return false;
  }
  assert i > 0;
  assert ! (perm[i-1] >= perm[i]);

  var j : int := perm.Length - 1;

  while perm[j] <= perm[i-1]
    decreases j - i
    invariant j >= i
  {
    j := j-1;
  }

  ghost var pperm : seq <nat> := perm[..];

  var temp : int := perm[i-1];
  perm[i-1] := perm[j];
  perm[j] := temp;

  forall k | 1 <= k <= perm.Length ensures k in perm[..]
  {
    contains_implies_index(k, pperm);
    var m :| 0 <= m < perm.Length && pperm[m] == k;
    if k != perm[i-1] && k != perm[j] {
      assert perm[m] == k;
    }
  }

  j := perm.Length - 1;
  while i < j
    invariant 0 <= i < perm.Length
    invariant 0 <= j < perm.Length
    invariant forall k :: 1 <= k <= perm.Length ==> k in perm[..]
  {

    ghost var pperm : seq <nat> := perm[..];
    temp := perm[i];
    perm[i] := perm[j];
    perm[j] := temp;
    forall k | 1 <= k <= perm.Length ensures k in perm[..]
    {
      contains_implies_index(k, pperm);
      var m :| 0 <= m < perm.Length && pperm[m] == k;
      if k != perm[i] && k != perm[j] {
        assert perm[m] == k;
      }
    }
    i := i + 1;
    j := j - 1;
  }
  return true;
}