为何Dafny查找最大单调子数组方法的ensures子句无法证明？

一、定位证明失败场景的技术与工具 #

• 拆分后置条件：将复合的ensures子句拆分为多个独立断言，比如先验证索引合法性，再验证结果子数组的单调性，接着验证长度最优性，最后验证长度相同时的最左选择。拆分后可快速定位哪条条件未被证明。
• 插入调试断言：在循环关键节点（如每次迭代后、状态更新前后）添加assert语句，验证中间状态正确性。例如针对全相同元素场景，可添加：

  assert IsAllSame(a, currentStart, i);
  assert maxLength >= currentLength || (maxLength == currentLength && maxStart <= currentStart);
  

• 利用反例生成：Dafny验证失败时会自动生成反例，查看生成的测试用例（如全相同数组[3,3,3]、严格递增数组[1,2,3,4]），检查程序返回索引是否符合预期，对比后置条件约束。
• 运行测试用例：使用dafny run命令执行代码，传入边缘场景的测试数组，观察实际输出是否符合后置条件，排查逻辑执行与验证逻辑的差异。

二、代码修改方向 #

1. 修正单调判定逻辑 #

确保辅助函数的边界处理与索引范围和主方法的子数组长度计算一致。例如IsAllSame需覆盖闭区间内的所有元素：

function IsAllSame(a: array<int>, i: int, j: int): bool
  requires 0 <= i <= j < a.Length
{
  if i == j then true else a[i] == a[i+1] && IsAllSame(a, i+1, j)
}

同时明确IsMonotonic的定义：包含严格递增、严格递减或全相同三种情况。

2. 强化循环不变式 #

循环不变式是Dafny证明的核心，需覆盖已遍历部分的所有性质：

method FindLongestMonotonicSubarray(a: array<int>) returns (start: int)
  requires a.Length >= 1
  ensures 0 <= start < a.Length
  ensures let maxLen := a.Length - start;
          forall k, l: int :: 0 <= k <= l < a.Length && IsMonotonic(a, k, l) => (l - k + 1) <= (a.Length - start)
  ensures let maxLen := a.Length - start;
          forall k, l: int :: 0 <= k <= l < a.Length && IsMonotonic(a, k, l) && (l - k + 1) == maxLen => k >= start
{
  var currentStart := 0;
  var maxStart := 0;
  var maxLength := 1;
  var currentLength := 1;

  var i := 1;
  while i < a.Length
    invariant 1 <= i <= a.Length
    invariant 0 <= maxStart < a.Length
    invariant 1 <= maxLength <= i
    invariant 0 <= currentStart < i
    invariant 1 <= currentLength <= i - currentStart + 1
    invariant forall k, l: int :: 0 <= k <= l < i && IsMonotonic(a, k, l) => (l - k + 1) <= maxLength
    invariant forall k, l: int :: 0 <= k <= l < i && IsMonotonic(a, k, l) && (l - k + 1) == maxLength => k >= maxStart
  {
    if (IsStrictlyIncreasing(a, currentStart, i-1) && a[i-1] < a[i]) ||
       (IsStrictlyDecreasing(a, currentStart, i-1) && a[i-1] > a[i]) ||
       (IsAllSame(a, currentStart, i-1) && a[i-1] == a[i]) {
      currentLength := currentLength + 1;
    } else {
      if currentLength > maxLength {
        maxLength := currentLength;
        maxStart := currentStart;
      } else if currentLength == maxLength && currentStart < maxStart {
        maxStart := currentStart;
      }
      currentStart := i;
      currentLength := 1;
    }
    i := i + 1;
  }

  // 处理最后一段未比较的子数组
  if currentLength > maxLength {
    maxStart := currentStart;
  } else if currentLength == maxLength && currentStart < maxStart {
    maxStart := currentStart;
  }

  start := maxStart;
}

不变式需确保：已遍历部分中，最长子数组的长度不小于任何已检查子数组；长度相同时保留最左索引。

3. 显式处理边缘场景 #

针对全相同元素、整数组单调的场景，添加引理辅助证明：

Lemma EntireArrayIsMonotonic(a: array<int>)
  requires forall i: int :: 0 <= i < a.Length-1 => (a[i] < a[i+1] || a[i] > a[i+1] || a[i] == a[i+1])
  ensures IsMonotonic(a, 0, a.Length-1)
{
  // 证明整数组满足单调定义
}

Lemma AllSameArrayMaxLength(a: array<int>)
  requires forall i, j: int :: 0 <= i <= j < a.Length => a[i] == a[j]
  ensures forall k, l: int :: 0 <= k <= l < a.Length => (l - k + 1) <= a.Length
{
  // 证明全相同数组的最长子数组为自身
}

在主方法中调用这些引理，帮助Dafny完成边缘场景的证明。

4. 统一长度计算逻辑 #

确保子数组长度的计算（如l - k + 1）在后置条件、循环不变式、状态更新中完全一致，避免因索引边界（闭区间/左闭右开）导致的证明失败。

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