Dafny循环内调用方法报modifies clause错误且fresh不变量不可用如何解决

错误根因 #

报错的核心原因是两个规格声明缺失：

1. Add方法的modifies子句声明不全：你在Add实现中修改了原队列尾节点tl的next字段，但modifies里只写了队列对象this和ghost变量nodes，没有包含被修改的尾节点对象tl，Dafny无法确认该修改操作是合法的。
2. Foo方法的modifies子句没有覆盖队列原有节点的修改权限：Foo接收的q可能携带预分配节点，你需要明确声明允许修改这些原有节点的字段。

修复方案 #

第一步：修正Add方法的规格

给Add的modifies子句加上tl，明确该方法只会修改队列自身、ghost变量nodes、以及当前队列的尾节点对象：

method Add(d: int)  // add another node
  requires invar()
  ensures invar()
  ensures
    nodes != [] && nodes[.. |nodes| - 1] == old(nodes) &&
    fresh(nodes[|nodes| - 1])
  modifies this, nodes, tl  // 新增tl到modifies集
{
  var l: LL := new LL(d);
  tl.next := l;
  tl := l;
  nodes := nodes + [l];
}

第二步：完善Foo方法的规格和循环不变量

给Foo的modifies子句加上队列原有所有节点的修改权限，再补充循环不变量，说明新增的节点都是当前上下文创建的，天然具备修改权限：

method Foo(q: Queue)
  requires q.invar()
  modifies q, q.nodes, set n | n in q.nodes :: n  // 允许修改q的所有原有节点
{
  var i: nat := 0;
  while (i < 10)
    invariant i <= 10
    invariant q.invar()
    // 补充不变量：队列中除初始原有节点外，后续新增节点都在当前方法内创建，天然具备修改权限
    invariant forall n | n in q.nodes && n !in old(q.nodes) :: fresh(n)
    decreases 10 - i
  {
    q.Add(i);
    i := i + 1;
  }
}

如果要提升扩展性，也可以给Queue类新增一个ghost类型的footprint: set<object>字段，在不变量中维护footprint == set n | n in nodes :: n，后续所有相关方法的modifies只要写this, nodes, footprint即可，不需要每次枚举节点集合。

内容的提问来源于stack exchange，提问作者Alley Stoughton