Request: sorting

[robin-aws]

I whipped up a quick mergesort implementation for the new dafny-reportgenerator tool, but more for fun than because I thought it was the absolute best default choice of algorithm for any Dafny user: https://github.com/dafny-lang/dafny-reportgenerator/blob/main/src/StandardLibrary.dfy#L38 There are lots of sorting algorithm implementations floating around in Dafny, including at least 4 in the regression suite. :) But there should be a sensible default implementation in the standard library.

I'd suggest implementing these signatures (with the appropriate pre- and post-conditions), for maximum flexibility (Edit: avoid requiring T<0> by using ToArray):

  method SortArray<T>(a: array<T>, compare: (T, T) -> bool) {
    ...
  }

  function Sort<T>(s: seq<T>, compare: (T, T) -> bool): seq<T> {
    ...
  } by method {
    var a := Seq.ToArray(s);  // From https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sequences/Seq.dfy#L128
    SortArray(a, compare);
    return a[..];
  }

I'd recommend implementing Musser's Introspective Sort, which is becoming the standard: https://en.wikipedia.org/wiki/Introsort. I'd be happy with just a heapsort to start with, though, as it has the most predictable runtime and minimal space overhead if you're starting with a mutable array. We can always add the optimization of quicksort-until-it-tends-quadratic later.

Another wrinkle is how to parameterize by the comparison function. Expressing the total ordering requirements using forall expressions is easy IF we assume T is not a reference type, but I expect that will be limiting. Perhaps it's feasible to require the comparison function is a total ordering just over all values being sorted, rather than all possible T values?

[RustanLeino]

A way to write the ordering requirements today is to quantify only over the elements of the array. For example,

forall x :: x in a[..] ==> compare(x, x) // reflexivity

[cpitclaudel]

I'd recommend implementing Musser's Introspective Sort,

Or https://en.wikipedia.org/wiki/Timsort , which historically had a bug that was found using formal methods ^^

[robin-aws]

We have https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sequences/MergeSort.dfy now, and #54 as a request for something more efficient, so we can close this.