Дафни селекция сортировка по убыванию - PullRequest
Новая
       10

Дафни селекция сортировка по убыванию

0 голосов
/ 24 мая 2018

У меня есть следующий метод для выполнения сортировки выбора в в порядке убывания .Однако говорят, что самый первый инвариант в цикле 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;
        }
    }

1 Ответ

0 голосов
/ 24 мая 2018

Возможно, сравнение a[index] < a[minIndex] неверно.Вы пытаетесь переместить маленький материал вправо, поэтому, если a[minindex] меньше a[index], вам нужно переместить его (a[minindex]) вправо.

...