dafny - 在 dafny 中覆盖数组

Question

我正在尝试覆盖方法内的数组。编译器给我错误“错误：赋值的 LHS 必须表示一个可变变量”。

    method invalidSort(a : array<int>)
    modifies a;
    requires a != null;
    ensures sorted(a[..]);
    {
       a := new int[0];
    }

我是在盯着自己瞎看，错过了什么，还是达夫尼不允许这样做？

Answer 1

在 Dafny 中，无法分配方法参数。如果需要在内部更新值，可以使用局部变量。

例如，

var a' := new int[0];

如果您希望调用者可以使用这个新数组，您还需要返回它。

return a';    

综上所述，如果您正在尝试编写就地排序方法，那么您无需执行任何操作。原地修改a即可。

a[0] := 0;
// ...