如何在Dafny中实现方法并确保未访问数组元素保持不变

下面给出一个可验证的实现示例，以“将数组前m个元素加1”为例，确保方法满足指定的后置条件：

method AddOneToFirstM(a: array<int>, m: int)
  requires 0 ≤ m ≤ a.Length
  ensures forall i: int :: m < i ≤ a.Length ==> old(a[i]) == a[i]
{
  var i := 0;
  while i < m
    invariant 0 ≤ i ≤ m
    invariant forall j: int :: m < j ≤ a.Length ==> old(a[j]) == a[j]
    invariant forall j: int :: 0 ≤ j < i ==> a[j] == old(a[j]) + 1
  {
    a[i] := a[i] + 1;
    i := i + 1;
  }
}

关键说明： #

• 前置条件：requires 0 ≤ m ≤ a.Length 用来约束m的合法范围，避免数组越界，同时确保“m之后的元素”这个范围是有效的。
• 循环不变式：
  • 第一个不变式跟踪循环变量i的范围，保证循环只在前m个元素内执行。
  • 第二个不变式是核心：它声明在整个循环过程中，所有m之后的元素始终等于初始值。Dafny会验证循环体的操作从未触及这些元素，因此循环结束后自然满足方法的后置条件。
  • 第三个不变式记录已处理元素的状态，保证方法的功能正确性（前m个元素确实完成了加1操作）。
• 循环体：仅对索引从0到m-1的元素进行修改，完全不会访问m及之后的元素，结合不变式的约束，Dafny可以自动完成后置条件的验证。

如果需要实现其他仅修改前m个元素的逻辑，只需要调整循环体的操作，并同步修改对应的功能不变式即可，核心是保留“m之后元素不变”的那个循环不变式，同时保证循环操作的范围不超过前m个元素。

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