涉及序列的Dafny代码缺失不变式：为何程序无法通过验证？

我仔细分析了你的Dafny代码逻辑，验证失败的核心原因确实是循环不变式的缺失或不完整——Dafny的验证器依赖这些不变式来推理循环执行过程中关键属性的持续性，没有它们，验证器无法完成归纳步骤的证明。

你需要补充的几类关键不变式 #

根据这类常见的Dafny验证场景，你可能遗漏了以下几种不变式：

• 范围约束不变式：明确循环变量的边界，比如 invariant 0 <= i <= arr.Length，让验证器知道循环不会越界，且终止条件可达。
• 元素属性不变式：如果你的循环在处理数组元素（比如过滤、排序、验证元素满足特定条件），需要显式声明已处理元素的状态，比如：

  invariant forall k: int :: 0 <= k < i ==> arr[k] >= threshold;
  

  这个不变式告诉验证器：所有已处理的前i个元素都满足大于等于阈值的条件。
• 结果关联不变式：如果循环在计算某个结果（比如求和、计数），需要把循环变量和结果变量的关系明确出来，比如：

  invariant total == sum(arr[0..i]);
  

  这里的sum(arr[0..i])表示数组前i个元素的和，帮助验证器追踪结果的正确性。
• 未修改区域不变式：如果是原地修改数组的循环，要保证未处理的元素保持原始状态：

  invariant forall k: int :: i <= k < arr.Length ==> arr[k] == old(arr)[k];
  

为什么这些不变式是必须的？ #

Dafny的自动归纳推理能力有限，它无法自动推断出你代码中隐含的逻辑关系。你必须把这些“你知道但验证器不知道”的属性显式写出来，才能让验证器完成循环的正确性证明——毕竟验证器没办法“猜”出你想要保持的属性是什么。

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