在dafny中修改返回变量

问题描述

所以我在dafny中有一个方法，它接收数组a，并返回排序后的版本b。在我的代码中，b：= a，然后就地插入排序发生在b上。但是，每当我修改b时，都会出现一个错误，即“赋值可能会更新不在封闭上下文的modify子句中的数组元素”。我假设这是因为我没有告诉dafny我将就地修改b。我该如何解决？

解决方法

Dafny中的

数组是对数组元素的引用。 （在C，Java，C＃和其他各种语言中也是如此。）赋值b := a;复制引用，但不复制元素。您有两种选择。

一种选择是创建一个新数组，该数组最终将保存排序后的元素。为此，分配一个新数组：

b := new int[a.Length];

如果您还想将a的元素复制到新数组b中，请执行以下操作：

b := new int[a.Length](i requires 0 <= i < a.Length reads a => a[i]);

或

b := new int[a.Length];
forall i | 0 <= i < a.Length {
  b[i] := a[i];
}

在此选择下，调用方仍将具有对原始数组的引用，该数组将保持不变。通过该方法的外参数，调用方还将获得对新（排序）数组的引用。

另一个选择是修改原始数组。由于这会影响调用者，因此您需要编写一个规范，以告知调用者有关此问题的信息。通过添加

来完成

modifies a

根据您的方法规范。在这种选择下，没有理由声明输出参数b，因为只有一个数组并且a引用了它。