Selection Sort in Dafny

I am trying to implement selection sort in Dafny.

My sorted and FindMin functions do work, but selectionsort itself contains assertions which Dafny will not prove, even if they are correct.

Here is my program:

predicate sorted(a:array<int>,i:int)
  requires a != null;
  requires 0 <= i <= a.Length;
  reads a;
{
  forall k :: 0 < k < i ==> a[k-1] < a[k]
}
method FindMin(a:array<int>,i:int) returns(m:int)
  requires a != null;
  requires 0 <= i < a.Length;
  ensures i <= m < a.Length;
  ensures forall k :: i <= k < a.Length ==> a[k] >= a[m];
{
  var j := i;
  m := i;
  while(j < a.Length)
    decreases a.Length - j;
    invariant i <= j <= a.Length;
    invariant i <= m < a.Length;
    invariant forall k :: i <= k < j ==> a[k] >= a[m];
  {
    if(a[j] < a[m]){m := j;}
    j := j + 1;
  }
}
method selectionsort(a:array<int>) returns(s:array<int>)
  requires a != null;
  modifies a;
  ensures s != null;
  ensures sorted(s,s.Length);
{
  var c,m := 0,0;
  var t;
  s := a;
  assert s != null;
  assert s.Length == a.Length;
  while(c<s.Length)
    decreases s.Length-c;
    invariant 0 <= c <= s.Length;
    invariant c-1 <= m <= s.Length;
    invariant sorted(s,c);
  {
    m := FindMin(s,c);
    assert forall k :: c <= k < s.Length ==> s[k] >= s[m];
    assert forall k :: 0 <= k < c ==> s[k] <= s[m];
    assert s[c] >= s[m];
    t := s[c];
    s[m] := t;
    s[c] := s[m];
    assert s[m] >= s[c];
    assert forall k :: c <= k < s.Length ==> s[k] >= s[c];
    c := c+1;
    assert  c+1 < s.Length ==> s[c-1] <= s[c];
  }
}

Why is this wrong? What does "postcondtion may not hold" mean? Could Dafny give an counter-example?

Solution

You seem to understand the basic idea behind loop invariants, which is needed to verify programs using Dafny.

Your program is not correct. One way to discover this is to use the verification debugger inside the Dafny IDE in Visual Studio. Click on the last error reported (the assertion on the line before the increment of c) and you will see that the upper half of the array contains an element that is smaller than both s[c] and s[m]. Then select the program points around your 3-statement swap operation and you will notice that your swap does not actually swap.

To fix the swap, exchange the second and third statement of the 3-statement swap. Better yet, make use of Dafny's multiple assignment statement, which makes the code easier to get right:

s[c], s[m] := s[m], s[c];

There are two other problems. One is that the second assertion inside the loop does not verify:

assert forall k :: 0 <= k < c ==> s[k] <= s[m];

While s[m] is the smallest element in the upper part of the array, the loop invariant needs to document that the elements in the lower part of the array are no greater than the elements in the upper part--an essential property of the selection sort algorithm. The following loop invariant does the trick:

invariant forall k, l :: 0 <= k < c <= l < a.Length ==> s[k] <= s[l];

Finally, the complaint about the property sorted(s,c) not being maintained by the loop stems from the fact that you defined sorted as strictly increasing, which swapping will never achieve unless the array's elements are initially all distinct. Dafny thus points out a design decision that you have to make about your sorting routine. You can either decide that your selectionsort method will apply only to arrays with no duplicate elements, which you do by adding

forall k, l :: 0 <= k < l < a.Length ==> a[k] != a[l];

as a precondition to (and loop invariant in) selectionsort. Or, more conventionally, you can fix your definition of sorted to replace a[k] > a[m] with a[k] >= a[m].

To clean up your code a little, you can now delete all assert statements and the declaration of t. Since m is used only inside the loop, you can move the declaration of m to the statement that calls FindMin, which also makes it evident that the loop invariant c-1 <= m <= s.Length is not needed. The two decreases clauses can be omitted; for your program, Dafny will supply these automatically. Lastly, your selectionsort method modifies the given array in place, so there is no real reason to return the reference a in the out-parameter s; instead, you can just omit the out-parameter and replace s by a everywhere.