Dafny 选择排序降序

Question

我有以下方法以降序执行选择排序。但是while循环中的very first invariant据说循环不维护，为什么会这样？

 method sortDesc (a : array<int>) 
        modifies a;
        requires a != null;
        ensures forall m,n :: 0 <= m < n < a.Length ==> a[m] >= a[n];
        requires a.Length > 1;
        ensures multiset(a[..]) == multiset(old(a[..]));
    {
        var index := a.Length - 1;
        while(index > -1)
            invariant forall m,n :: 0 <= m <= index && index < n < a.Length ==> a[m] >= a[n];               // all elements that we have not sorted are bigger than any element we have sorted  !!!!!!!!!!!!
            invariant a.Length > index > -1;
            invariant forall k,l :: index < k < l < a.Length ==> a[k] >= a[l];                              //the part we have gone through is already sorted!!
            invariant multiset(a[..]) == multiset(old(a[..]));                                      // USED TO MAKE SURE ALL THE STARTING ELEMENTS ARE STILL THERE!!!!!
            decreases index;
        {
            var minIndex := findMinBetween(a, index, a.Length);
            if (a[index] < a[minIndex]) 
            {
                a[index], a[minIndex] := a[minIndex],a[index];                               //SWAP ELEMENTS!!!
            }
            if (index == 0)
            {
                return;
            }
            index := index - 1;
        }
    }

Answer 1

也许比较 a[index] < a[minIndex] 是错误的方式。您正在尝试将小东西向右移动，因此如果 a[minindex] 小于 a[index] 您需要将它 (a[minindex]) 向右移动。

Dafny 选择排序降序

Dafny selection sort descending

arrays

selection-sort

dafny