Дафни, присваивая секвенцию последовательности массиву - PullRequest
Новая
       26

Дафни, присваивая секвенцию последовательности массиву

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

в моей программе 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

1 Ответ

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

Что вам нужно сделать, это присвоить выходные данные метода 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] находится в диапазоне.

...