Dafny中初始化整数数组报错：调用可能违反上下文修改子句

错误原因 #

你的init方法的modifies子句仅写了intarray，但Dafny需要明确该数组属于当前类的实例对象。这种写法没有关联到具体实例，导致调用sh.init(4)时，Dafny无法确认该调用有权修改sh对象的字段，从而触发"call might violate context's modifies clause"错误。

修复方案 #

将init方法的modifies子句改为以下两种写法之一：

• modifies this：表示允许修改当前对象的所有字段
• modifies this.intarray：更精确地指定仅修改当前对象的intarray字段

修改后的完整代码 #

class shap {
  var intarray: array<int>; 
  constructor (i: int) 
    requires i > 0
  {
      this.intarray := new int[i];
  }
  method init(i: int)
    modifies this.intarray  // 可替换为 modifies this
  {
    var index: int := 0;
    while (index < intarray.Length) {
      intarray[index] := i;
      index := index + 1;
    }
  }
}

method Main() {
  var sh := new shap(5);
  sh.init(4);
}

修改后，Dafny能明确init方法的修改范围，Main方法中的调用就符合约束要求，错误会被消除。

内容的提问来源于stack exchange，提问作者Abdallah Rayhan