在dafny中修改返回变量

Question

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

Answer 1

Dafny中的数组是对数组元素的引用。(在C、Java、C#和各种其他语言中也是如此。)assignment 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];
}

在此选择下，调用方仍将拥有对原始数组的引用，该数组将保持不变。通过该方法的out参数，调用者还将获得对新(排序的)数组的引用。

另一种选择是修改原始数组。由于这会影响调用者，因此您需要编写一个规范来告诉调用者这一点。这可以通过添加

modifies a

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