Selection Sort in Dafny

Question

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,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,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) returns(s:array) 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

Accepted Answer

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.

Selection Sort in Dafny

Solution

Problem