在 dafny 中修改返回变量

Question

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

Answer 1

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 引用了它。