Given the usual specification of array sorting in Dafny,
method sort(a: array<T>)
modifies a
ensures isSorted(a[..])
ensures multiset(a[..]) == multiset(old(a[..]))
predicate isSorted(s: seq<T>) {
forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j]
}
Dafny is able to check a "test case" without duplicates (with a small help)
method testSortWithoutDups() {
var a := new T[] [9, 4, 6, 3, 8];
assert a[..] == [9, 4, 6, 3, 8]; // small prover helper!
sort(a);
assert a[..] == [3, 4, 6, 8, 9];
}
But is not able to check a "test case" with duplicates, so I tried using a lemma as follows:
method testSortWithDups() {
var a := new T[] [9, 3, 6, 9];
assert a[..] == [9, 3, 6, 9]; // small prover helper!
sort(a);
SortingProp(a[..], [3, 6, 9, 9]);
assert a[..] == [3, 6, 9, 9];
}
// State and prove by induction the property that, if two sequences are sorted and have
// the same elements, then they must be identical (so sorting has a unique solution).
// Most of the proof steps are filled in by Dafny.
lemma SortingProp(a: seq<T>, b: seq<T>)
requires isSorted(a) && isSorted(b) && multiset(a) == multiset(b)
ensures a == b
{
seqProps(a);
seqProps(b);
if |a| > 0 {
SortingProp(a[1..], b[1..]);
}
}
// Two usefull properties about sequences and their multisets (proved by Dafny alone):
lemma seqProps(a: seq<T>)
ensures |a| > 0 ==> a == [a[0]] + a[1..]
ensures forall i :: 0 <= i < |a| ==> a[i] in multiset(a)
{}
Is there a better solution?
