Дафни, назначение фрагмента последовательности массиву

в моей программе Dafny у меня есть массив input:array?<int> с четной длиной, который я хочу разрезать на две равные части, отсортировать их по отдельности и затем объединить в упорядоченном порядке. (сортировка вставками в уже реализованном и проверенном массиве целых чисел). нарезка и слияние в Dafny с seq<int> очень просты, а полная документация по ним находится в rise4fun. но я не мог найти простой подход к массивам. Как проще всего сделать то же самое, что и последовательности с массивом?

        method MySort(input:array?<int>)
        { var mid:= input.Length/2;
          var subOne := input[0..mid];
          var subTwo := input[mid..input.Length];
          insertionSort(subOne); // ofcourse ERROR as insertion sort is implemented for array<int>
          insertionSort(subTwo); // ofcourse ERROR as insertion sort is implemented for array<int>
          input := subTwo + subOne;
        }

полный код находится здесь, вrise4fun, в этом коде я закомментировал подход к последовательности и сделал некоторые нарезки с циклом while. если это лучший способ сделать, как мне потом выполнить конкатенацию.

Также Здесь я сделал метод сортировки с seq<int>, но в части обмена (input[j := b]; input[j-1 := a];) я также получаю expected method call, found expression . Согласно учебнику input[j:=b] следует заменить индекс j ввода seq значением b


verification z3 dafny
person Amir-Mousavi    schedule 19.05.2018    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Что вам нужно сделать, так это присвоить результат метода insertionSort такой переменной:

subOne := insertionSort(subOne); 
subTwo := insertionSort(subTwo);

Теперь у вас будет проблема на следующей строке

input := subTwo + subOne;

потому что

subOne + subTwo

— это последовательность, а input — это указатель на массив. Вы не хотите менять указатель, вы хотите изменить содержимое массива. Один из способов сделать это показан ниже:

method probOneSort(input:array?<int>) 
modifies input;
requires input != null;
requires input.Length > 0;
requires input.Length%2==0;
{
 var mid:= input.Length/2;

 var subOne := input[0..mid];
 var subTwo := input[mid..input.Length];

 subOne := insertionSort(subOne);
 subTwo := insertionSort(subTwo);

 var val := subOne + subTwo ;
 forall i | 0 <= i && i < input.Length { input[i] := val[i] ; }
}

Чтобы это проверить, вам нужно, чтобы insertionSort гарантировал, что длина его вывода будет такой же, как длина его ввода. В противном случае верификатор не сможет проверить, находится ли индекс val[i] в диапазоне.

person Theodore Norvell    schedule 21.05.2018
comment
обычно лучше изменить сортировку вставки на последовательность (с которой теперь у меня проблемы с изменчивостью и нарушением функций). или сохранить его как массив «int» и изменить подход в методе probOneSort? образцы кода один или два? как лучше? - person Amir-Mousavi; 22.05.2018
comment
Для эффективности использование массивов даст более эффективный алгоритм. Для проверки последовательности немного проще, потому что массивы дают косвенный доступ к местоположениям; это означает, что вам нужно узнать о reads и modifies, чтобы использовать массивы. - person Theodore Norvell; 23.05.2018