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

我怎样才能（用达夫尼语）陈述“ensures“保证方法返回的对象将是“新的”，即不会与其他地方使用的对象相同（尚未）？

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

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;
  }


}

The "doeswork" 函数正确编译（并验证），但另一个函数则不然，因为 Dafny 编译器无法知道 " 返回的对象newArray" 功能是新的，即不需要在 " 的 "require" 语句中列为可修改的不起作用“函数，以便该函数满足它仅修改的要求”this“。 在里面 ”doeswork“函数，我只是插入了”的定义newArray” 函数，然后就可以了。

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

Thanks!

你可以说ensures fresh(b) on newArray.

fresh正是您所描述的意思：该对象与调用之前分配的任何对象都不同newArray.