Dafny迭代计算自然数序列最大值：循环不变量正确性咨询

问题分析 #

你从序列起始位置遍历的思路是正确的，循环不变量max == maximo(s[..i])逻辑上没问题，但Dafny无法自动验证循环体执行后该不变量仍然成立——这是因为需要证明序列前缀扩展后的最大值等于原前缀最大值与新元素的最大值，而这个性质需要手动添加引理来确认。

核心引理 #

要让Dafny认可你的不变量，需要先证明以下引理：

lemma maximo_prefix_extend(s: seq<nat>, n: nat)
  ensures maximo(s + [n]) == max(maximo(s), n)
{
  if s == [] {
    assert maximo([] + [n]) == n;
    assert max(maximo([]), n) == max(0, n) == n;
  } else {
    calc {
      maximo(s + [n]);
      if s[0] > maximo(s[1..] + [n]) then s[0] else maximo(s[1..] + [n]);
      if s[0] > max(maximo(s[1..]), n) then s[0] else max(maximo(s[1..]), n);
      max(max(s[0], maximo(s[1..])), n);
      max(maximo(s), n);
    }
  }
}

这个引理通过归纳法证明：给任意序列追加一个元素后，新序列的最大值等于原序列最大值和该元素的最大值，填补了Dafny自动推导的空白。

修正后的完整代码 #

将引理加入你的代码，并在循环体中补充验证逻辑，让Dafny确认不变量的维护：

function maximo(s: seq<nat>): nat
  decreases |s|
{
  if s == [] then 0 else if s[0] > maximo(s[1..]) then s[0] else maximo(s[1..])
}

lemma maximo_prefix_extend(s: seq<nat>, n: nat)
  ensures maximo(s + [n]) == max(maximo(s), n)
{
  if s == [] {
    assert maximo([] + [n]) == n;
    assert max(maximo([]), n) == max(0, n) == n;
  } else {
    calc {
      maximo(s + [n]);
      if s[0] > maximo(s[1..] + [n]) then s[0] else maximo(s[1..] + [n]);
      if s[0] > max(maximo(s[1..]), n) then s[0] else max(maximo(s[1..]), n);
      max(max(s[0], maximo(s[1..])), n);
      max(maximo(s), n);
    }
  }
}

method maximo_it(s: seq<nat>) returns (max: nat)
  ensures max == maximo(s);
{
  max := 0;
  var i := 0;

  while i < |s|
    decreases |s| - i
    invariant 0 <= i <= |s|
    invariant max == maximo(s[..i])
  {
    var old_max := max;
    var old_i := i;
    
    if old_max < s[old_i] {
      max := s[old_i];
    }
    i := old_i + 1;

    // 利用引理证明新的max满足不变量
    assert max == max(old_max, s[old_i]);
    maximo_prefix_extend(s[..old_i], s[old_i]);
    assert maximo(s[..old_i+1]) == max(maximo(s[..old_i]), s[old_i]);
    assert max == maximo(s[..i]);
  }
}

说明 #

• 初始状态i=0时，s[..0]是空序列，maximo([])=0，与max的初始值一致，满足不变量。
• 循环体中，通过引理推导得出：更新后的max等于maximo(s[..i+1])，确保每次循环后不变量仍然成立。
• 循环结束时i=|s|，此时max == maximo(s[..|s|])，即max == maximo(s)，满足方法的后置条件。

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