为何第二个循环不变式在进入循环时不成立？

你的第二个循环不变式在理论上初始时是成立的，但可能Dafny的验证器无法自动完成推导，或者你对不变式的预期与验证器的证明路径不匹配。我们来拆解分析：

初始状态的等式验证 #

初始时i=0，k=a.Length，此时：

• a[..i]是空序列[]，a[k..]也是空序列[]
• a[i..k]等价于整个数组的序列，即old(a[..])（因为数组还未被修改）

代入不变式：

reverse(old(a[..])) == [] + reverse(old(a[..])) + []

显然等式两边完全相等，所以初始状态下不变式是成立的。

验证器无法证明的可能原因 #

Dafny的自动验证器对递归定义的函数（比如你自定义的reverse）的等式推导需要明确的性质支撑，可能需要你补充辅助引理或调整不变式写法，帮助验证器完成证明：

1. 补充reverse函数的性质引理

你可以为reverse函数添加一些基础性质的引理，帮验证器理解其拼接与反转的关系：

lemma reverse_idempotent(s: seq<int>)
ensures reverse(reverse(s)) == s
{
  if s == [] {}
  else {
    reverse_idempotent(s[..|s|-1]);
    assert reverse(reverse(s)) == reverse([s[|s|-1]] + reverse(s[..|s|-1]));
    assert reverse([s[|s|-1]] + reverse(s[..|s|-1])) == reverse(reverse(s[..|s|-1])) + [s[|s|-1]];
  }
}

lemma reverse_append(s: seq<int>, t: seq<int>)
ensures reverse(s + t) == reverse(t) + reverse(s)
{
  if s == [] {}
  else {
    reverse_append(s[..|s|-1], t);
    assert reverse(s + t) == reverse((s[..|s|-1] + [s[|s|-1]]) + t);
    assert reverse((s[..|s|-1] + [s[|s|-1]]) + t) == reverse((s[..|s|-1] + t) + [s[|s|-1]]);
    assert reverse((s[..|s|-1] + t) + [s[|s|-1]]) == [s[|s|-1]] + reverse(s[..|s|-1] + t);
  }
}

2. 拆分循环不变式为更易验证的子条件

将原有的复合不变式拆分为三个独立的子不变式，验证器更容易逐个证明：

while k > i + 1
  invariant 0 <= i <= k <= a.Length
  invariant reverse(old(a[..]))[..i] == a[..i]
  invariant reverse(old(a[..]))[k..] == a[k..]
  invariant reverse(old(a[..]))[i..k] == reverse(a[i..k])

• 前两个不变式明确：已处理的左右两段已经是原数组反转后的对应部分
• 第三个不变式明确：未处理的中间段的反转等于原数组反转后的中间段

这种拆分后的不变式，初始状态下的证明会更直接，循环迭代后的维护也更容易被验证器识别。

总结 #

你的原不变式在初始状态下逻辑上是成立的，问题出在Dafny验证器无法自动递归推导reverse函数的等式关系。通过补充引理或拆分不变式，可以让验证器完成证明。

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