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

本文是小编为大家收集整理的关于在更改的对象上修改子句错误的处理方法,想解了在更改的对象上修改子句错误的问题怎么解决?在更改的对象上修改子句错误问题的解决办法?那么可以参考本文帮助大家快速定位并解决问题。

问题描述

如何陈述(在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;
  }


}

" domwork "函数正确编译(并验证)正确,但另一个没有,因为dafny编译器无法知道" newArray 返回的对象"函数是新的,即不需要列为"需要"的"需要"语句" donnotwork "功能中的可修改,以便实现该功能,以满足它只修改的要求"这个".在" waywork "函数中,我只是插入了" newArray "函数的定义,然后它工作.

您可以在 https://rise4fun.com/dafny/hwwwr ,它也可以在线运行.

谢谢!

推荐答案

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

fresh意味着您所描述的内容:对象与在呼叫到newArray之前分配的任何对象不同.

本文地址:https://www.itbaoku.cn/post/1793855.html