如何编写Dafny的modifies子句以避免冗余的unchanged后置条件？

Dafny完全支持在modifies子句中精确指定要修改的对象字段，不需要将整个对象纳入修改范围。针对你的场景，只需调整modifies子句的写法即可实现需求。

核心语法说明 #

要指定修改序列中所有对象的某个字段，使用集合表达式：

modifies set a.x | a in this.l

这个表达式明确声明：方法仅修改l序列中每个A实例的x字段，不会触及其他字段（比如y）。

修正后的完整代码 #

class A {
  var x : int
  var y : int
}

class B {
  const l : seq<A>

  method m()
      // 精确指定修改l中所有A实例的x字段
      modifies set a.x | a in this.l
      ensures forall a :: a in this.l ==> a.x == 10
      // 以下断言可省略，因为modifies已限定仅修改x，Dafny会自动验证y未被修改
      // ensures forall a :: a in this.l ==> unchanged(a.y)
  {
     var it := 0;
     while it < |this.l|
          invariant 0 <= it <= |this.l|
          invariant forall a :: a in this.l[..it] ==> a.x == 10
          // 同样，此处的unchanged断言可省略，modifies已覆盖该约束
          // invariant forall a :: a in this.l ==> unchanged(a.y)
      {
          this.l[it].x := 10;
          it := it + 1;
      }
  }
}

关键细节 #

1. 避免错误的modifies范围：原代码中的modifies l是错误的，因为l是const序列，本身不可修改；你真正要修改的是序列中对象的字段，而非序列本身。
2. 自动验证未修改字段：当modifies子句明确指定了要修改的字段后，Dafny会自动检查其他字段（比如y）是否保持不变，因此无需额外写unchanged断言，除非你想显式强调这一点。
3. 循环不变式简化：循环中的unchanged(a.y)断言也可省略，因为modifies的范围约束已经保证了这一点，Dafny会自动验证。

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