Dafny，将序列切片分配给数组

Question

在我的 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;
        }

完整的代码是here in rise4fun，在这段代码中我注释掉了sequence approch，并用while循环做了一些切片。如果这是最好的方法，我应该如何进行连接。

另外Here 我用seq<int> 做了排序方法但是在交换部分（input[j := b]; input[j-1 := a];）我也得到了expected method call, found expression。根据教程 input[j:=b] 应该用 b

的值替换 seq 输入的索引 j

Answer 1

您需要做的是将 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]是否在范围内。

Dafny，将序列切片分配给数组

Dafny, assigning sequence slice to array

z3

verification

dafny