automated-tests - 修改已更改对象的子句错误

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”返回的对象"函数是新函数，即不需要在“不工作”函数的“require”语句中列为可修改，以便该函数满足仅修改“这个”。在“doeswork”函数中，我简单地插入了“newArray”函数的定义，然后它就起作用了。

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

谢谢!

Answer 1

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

fresh 的意思正是您所描述的:该对象不同于调用 newArray 之前分配的任何对象。