时间戳

首页 > 解决方案 > Dafny，将序列切片分配给数组

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

问题描述

在我的 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]应该用 b 的值替换 seq 输入的索引 j

标签： z3verificationdafny

解决方案

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

推荐阅读