修改已更改对象的子句错误 [英] Modifies clause error on a changed object

问题描述

如何在Dafny中声明 确保，以保证方法返回的对象是新的，即与在其他任何地方使用的对象都不相同（

How can I state (in Dafny) an "ensures" guarantee that the object returned by a method will be "new", i.e., will not be the same as an object used anywhere else (yet)?

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

The following code shows a minimal example:

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语句中被列为可修改的，以便该函数满足仅修改 this 。在 doeswork 函数中，我只是插入了 newArray 函数的定义，然后它起作用了。

The "doeswork" function compiles (and verifies) correctly, but the other one does not, as the Dafny compiler cannot know that the object returned by the "newArray" function is new, i.e., is not required to be listed as modifiable in the "require" statement of the "doesnotwork" function in order for that function to fulfill the requirement that it only modifies "this". In the "doeswork" function, I simply inserted the definition of the "newArray" function, and then it works.

您可以在 https://rise4fun.com/Dafny/hHWwr 下找到上述示例，

You can find the example above under https://rise4fun.com/Dafny/hHWwr, where it can also be ran online.

谢谢！

推荐答案

您可以说确保 newArray 上的新鲜（b）。

You can say ensures fresh(b) on newArray.

新鲜的含义与您所描述的完全相同：该对象与调用之前分配的任何对象都不相同到 newArray 。

fresh means exactly what you described: the object is not the same as any object that was allocated before the call to newArray.

这篇关于修改已更改对象的子句错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！