修改已更改对象的子句错误

Question

我如何声明（在 Dafny 中）“确保”保证方法返回的对象将是“新的”，即与其他任何地方使用的对象不同（还是）？

以下代码显示了一个最小示例：

method newArray(a:array<int>) returns (b:array<int>)
requires a != null
ensures b != null
ensures a != b
ensures b.Length == a.Length+1
{
  b := new int[a.Length+1];
}

class Testing {
  var test : array<int>;

  method doesnotwork()
  requires this.test!=null
  requires this.test.Length > 10;
  modifies this
  {
    this.test := newArray(this.test); //change array a with b
    this.test[3] := 9;  //error modifies clause
  }

  method doeswork()
  requires this.test!=null
  requires this.test.Length > 10;
  modifies this
  {
    this.test := new int[this.test.Length+1];
    this.test[3] := 9;
  }


}

“doeswork”函数可以正确编译（并验证），但另一个没有，因为 Dafny 编译器无法知道“newArray”返回的对象" 函数是新的，即不需要在 "doesnotwork" 函数的 "require" 语句中列为可修改，以便该函数满足它只修改 " 的要求>这个”。在“doeswork”函数中，我只是简单的插入了“newArray”函数的定义，然后就可以工作了。

上面的例子可以在https://rise4fun.com/Dafny/hHWwr下找到，也可以在线运行。

谢谢！

Answer 1

你可以在newArray 上说ensures fresh(b)。

fresh 与您所描述的完全一样：该对象与调用newArray 之前分配的任何对象都不相同。