如何让单次遍历数组的Dafny迭代方法通过验证？

不用移除Min/Max函数，关键是给函数补全严谨的规范，并为迭代方法设计精准的循环不变式，就能通过验证。

1. 定义带完整规范的Min/Max函数 #

必须为函数补充前置条件（数组非空）和明确的后置条件，确保验证器能理解函数返回值的语义：

function Min(a: array<int>): int
  requires a.Length > 0
  // 所有元素都大于等于返回值
  ensures forall i :: 0 <= i < a.Length ==> Min(a) <= a[i]
  // 存在至少一个元素等于返回值
  ensures exists i :: 0 <= i < a.Length && Min(a) == a[i]
{
  if a.Length == 1 then a[0]
  else if a[a.Length-1] < Min(a[0..a.Length-1]) then a[a.Length-1]
  else Min(a[0..a.Length-1])
}

function Max(a: array<int>): int
  requires a.Length > 0
  // 所有元素都小于等于返回值
  ensures forall i :: 0 <= i < a.Length ==> Max(a) >= a[i]
  // 存在至少一个元素等于返回值
  ensures exists i :: 0 <= i < a.Length && Max(a) == a[i]
{
  if a.Length == 1 then a[0]
  else if a[a.Length-1] > Max(a[0..a.Length-1]) then a[a.Length-1]
  else Max(a[0..a.Length-1])
}

2. 单次遍历方法的验证实现 #

迭代方法的核心是用循环不变式将当前维护的currentMin/currentMax与子数组的Min/Max函数结果绑定，让验证器能推导出最终状态与整个数组的Min/Max的关系：

method SinglePassDiff(a: array<int>) returns (diff: int)
  requires a.Length > 0
  ensures diff == Max(a) - Min(a)
{
  var i := 1;
  var currentMin := a[0];
  var currentMax := a[0];

  while i < a.Length
    invariant 1 <= i <= a.Length
    // 明确当前min是前i个元素的最小值
    invariant currentMin == Min(a[0..i])
    // 明确当前max是前i个元素的最大值
    invariant currentMax == Max(a[0..i])
    // 辅助约束，帮助验证器推导
    invariant forall k :: 0 <= k < i ==> currentMin <= a[k] <= currentMax
  {
    if a[i] < currentMin {
      currentMin := a[i];
    }
    if a[i] > currentMax {
      currentMax := a[i];
    }
    i := i + 1;
  }

  diff := currentMax - currentMin;
}

关键验证逻辑说明 #

• Min/Max函数的两个后置条件是核心：全域约束确保返回值是数组的下界/上界，存在性约束确保返回值确实是数组中的元素，二者结合才能让验证器认可函数的语义。
• 循环不变式不能模糊描述“当前遍历过的元素的最小/最大”，必须直接绑定到Min(a[0..i])和Max(a[0..i])，让验证器能将迭代状态与函数规范关联起来，逐步推导出循环结束时currentMin等于Min(a)、currentMax等于Max(a)。
• 保留Min/Max函数反而能简化验证逻辑，纯函数的规范比直接用断言更清晰，不需要移除。

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