insertion_sort.dfy

// insertion_sort.dfy - An attempt to verify a simple O(n^2) insertion sort implementation

predicate sorted(a: seq<nat>)
{
  forall j, k :: 0 <= j < k < |a| ==> a[j] <= a[k]
}

// Find the point where a[i] could be inserted into a[..i] to keep it sorted.
//
// This could be switched to binary search without changing the signature,
// improving InsertionSort to O(n log n).
// Might be faster in practice to search backwards, on the theory that the data
// we're asked to sort is often already partly sorted.
//
method InsertionPoint(a: array<nat>, i: nat) returns (j: nat)
  requires i < a.Length && sorted(a[..i])
  ensures j <= i && sorted(a[..j] + [a[i]] + a[j..i])
{
  j := 0;
  assert !(j > 0);
  while j < i
    invariant j <= i
    invariant j > 0 ==> a[j - 1] < a[i]
  {
    if a[i] <= a[j] {
      break;
    }
    assert a[i] > a[j];
    j := j + 1;
    assert a[j - 1] < a[i];
  }
}

// Rotate a[start .. last + 1] one element to the right,
// so that a[last] ends up at a[start].
//
// The last postcondition asserts that this just rearranges elements
// without changing which ones are present in `a`.
//
method RotateRight(a: array<nat>, start: nat, last: nat)
  modifies a
  requires start <= last < a.Length
  ensures a[..] == old(a[..])[..start] + [old(a[..])[last]] + old(a[..])[start..last] + old(a[..])[last + 1..]
  ensures multiset(a[..]) == multiset(old(a[..]))
{
  ghost var orig := a[..];

  var new_value := a[last];  // the value to be moved left
  var i := last;
  while i > start
    invariant i >= start
    invariant a[..i] == orig[..i]
    invariant a[i + 1 .. last + 1] == orig[i .. last]
    invariant a[last + 1 ..] == orig[last + 1 ..]
  {
    i := i - 1;
    a[i + 1] := a[i];
  }
  assert i == start;
  assert a[..start] == orig[..start];
  assert a[start + 1 .. last + 1] == orig[start .. last];
  a[start] := new_value;
  assert a[start] == orig[last];
  assert a[..] == a[..start] + [a[start]] + a[start + 1 .. last + 1] + a[last + 1 ..];
  assert a[..] == orig[..start] + [orig[last]] + orig[start .. last] + orig[last + 1 ..];
  assert multiset(orig[..start] + orig[start .. last] + [orig[last]])
         == multiset(orig[..start] + [orig[last]] + orig[start .. last]);
  assert multiset(orig[..start] + orig[start .. last] + [orig[last]] + orig[last + 1..])
         == multiset(orig[..start] + [orig[last]] + orig[start .. last] + orig[last + 1 ..]);
  assert orig[..start] + orig[start .. last] + [orig[last]] + orig[last + 1..] == orig[..];
  assert multiset(orig[..]) == multiset(a[..]);
}

// Sort an array of natural numbers in place.
method InsertionSort(a: array<nat>)
  modifies a
  ensures sorted(a[..]) && multiset(a[..]) == multiset(old(a[..]))
{
  var i := 0;
  ghost var original_seq := a[..];
  while i < a.Length
    invariant 0 <= i <= a.Length
    invariant sorted(a[..i])
    invariant multiset(a[..]) == multiset(original_seq)
  {
    // a[..i] is already sorted; move a[i] left, if necessary, and insert it somewhere so that
    // a[..i+1] is then sorted.
    var j := InsertionPoint(a, i);
    RotateRight(a, j, i);
    i := i + 1;
  }
}