Dafny选择排序降序

Question

下面是以降序执行选择排序的方法。但是，在while循环中的第一个不变量据说不是由循环维护的，为什么会这样呢？

 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])移到右边。