Dafny循环不变量错误排查：最长平台实现问题求助

问题背景 #

针对《PROGRAM PROOFS》（K. Rustan M. Leino著）第13章第17题，需求如下：

• (a) 定义幽灵谓词Plateau(s, lo, hi)，表示序列s的子段s[lo..hi]是连续相等元素的平台
• (b) 规范一个方法，输入整数序列返回最长平台的长度
• (c) 实现该方法

原始代码 #

ghost predicate Plateau<T>(s: seq<T>, lo: int, hi: int)
  requires 0 <= lo <= hi <= |s|
{
  forall i, j :: lo <= i < j < hi ==> s[i] == s[j]
}

method LongestPlateau<T(==)> (s: seq<int>, lo: int, hi: int) returns (L: int)
  ensures 0 <= L <= |s|
  ensures forall lo, hi :: 0 <= lo <= hi <= |s| && Plateau(s, lo, hi) ==> L >= hi - lo
  ensures exists lo, hi :: 0 <= lo <= hi <= |s| && Plateau(s, lo, hi) && L == hi - lo
{
  var i: int := 0;
  L := 0;
  
  while i < |s|
    invariant 0 <= i <= |s|
    invariant 0 <= L <= |s|
    invariant forall lo, hi :: 0 <= lo <= hi <= i && Plateau(s, lo, hi) ==> L >= hi - lo
    invariant exists lo, hi :: 0 <= lo <= hi <= i && Plateau(s, lo, hi) && L == hi - lo
  {
    var f: int := i;
    

    while i < |s| && s[f] == s[i]
      invariant 0 <= f <= i <= |s|
      invariant forall j :: f < j < i ==> s[f] == s[j]
    {
      i := i + 1;      
    }
    
    if L < i - f {
      L := i - f;
    }
  }
  
}

错误描述 #

1. 外层循环的不变量forall lo, hi :: 0 <= lo <= hi <= i && Plateau(s, lo, hi) ==> L >= hi - lo无法被Dafny验证维持
2. 外层循环的不变量exists lo, hi :: 0 <= lo <= hi <= i && Plateau(s, lo, hi) && L == hi - lo无法通过循环前置条件验证（进入循环前不成立），且循环体执行后也无法维持

修复建议 #

1. 修正初始状态的矛盾 #

循环开始前i=0、L=0，此时lo=hi=0对应的空段是合法平台（空全称量词默认成立），但Dafny无法自动识别这一点。需要在方法开头添加断言辅助验证：

assert Plateau(s, 0, 0);

同时移除方法参数中未使用的lo和hi，修正泛型与参数类型不匹配的问题（原方法泛型为T但参数s是seq<int>）。

2. 调整内层循环的不变量 #

内层循环负责定位当前平台的结束位置，需要明确[f, i)是合法平台，添加Plateau(s, f, i)作为不变量，让Dafny能跟踪当前处理的段属性：

while i < |s| && s[f] == s[i]
  invariant 0 <= f <= i <= |s|
  invariant Plateau(s, f, i)
{
  i := i + 1;      
}

3. 强化外层循环的不变量验证 #

在更新L前，添加断言明确当前处理的[f, i)是平台，帮助Dafny推导新的L满足最长长度的要求：

assert Plateau(s, f, i);
if L < i - f {
  L := i - f;
}

完整修复后的代码 #

ghost predicate Plateau<T>(s: seq<T>, lo: int, hi: int)
  requires 0 <= lo <= hi <= |s|
{
  forall i, j :: lo <= i < j < hi ==> s[i] == s[j]
}

method LongestPlateau<T(==)> (s: seq<T>) returns (L: int)
  ensures 0 <= L <= |s|
  ensures forall lo, hi :: 0 <= lo <= hi <= |s| && Plateau(s, lo, hi) ==> L >= hi - lo
  ensures exists lo, hi :: 0 <= lo <= hi <= |s| && Plateau(s, lo, hi) && L == hi - lo
{
  var i: int := 0;
  L := 0;

  // 辅助初始状态验证
  assert Plateau(s, 0, 0);
  
  while i < |s|
    invariant 0 <= i <= |s|
    invariant 0 <= L <= |s|
    invariant forall a, b :: 0 <= a <= b <= i && Plateau(s, a, b) ==> L >= b - a
    invariant exists a, b :: 0 <= a <= b <= i && Plateau(s, a, b) && L == b - a
  {
    var f: int := i;

    while i < |s| && s[f] == s[i]
      invariant 0 <= f <= i <= |s|
      invariant Plateau(s, f, i)
    {
      i := i + 1;      
    }

    // 明确当前段是平台
    assert Plateau(s, f, i);
    if L < i - f {
      L := i - f;
    }
  }
}

关键修复点总结 #

• 添加初始断言，让Dafny识别空段作为合法平台
• 内层循环补充平台属性不变量，跟踪当前处理段的合法性
• 更新L前添加断言，辅助Dafny验证最长长度的维持性
• 修正方法参数与泛型的不匹配问题

内容的提问来源于stack exchange，提问作者2万で買った中古のパンツ