3

我如何声明（在 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;
  }


}

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

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

谢谢！

4

1 回答 1

3

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

fresh与您所描述的完全一样：该对象与在调用newArray.

于 2017-12-01T18:26:47.203 回答