Dafny 错误在未修改的数组上证明断言

Question

下面的 Dafny 方法只是断言对于每个索引 i，都存在一个索引 j，使得输入数组元素相等。我很好奇为什么特定的不变量和断言不成立，因为我没有修改数组。对达夫尼来说不是很明显吗？我是不是错过了什么？

method test(a:array<int>) returns (b:array<int>)
requires a.Length > 0
ensures b.Length > 0
ensures a.Length == b.Length
ensures forall k: int::0 <= k < a.Length ==> b[k] == a[k]
{
    var i:= 0;
    var j := 0;

    while i < a.Length
    invariant i >=0 && j>=0
    invariant i==j
    invariant i <= a.Length && j <= a.Length
    invariant forall k: int::0 <= k < i ==> exists l | 0 <= l < j:: a[k] == a[l]
    decreases (a.Length - i)
    decreases (a.Length - j)
    {
       assert forall k: int::0 <= k < i ==> exists l | 0 <= l < j:: a[k] == a[l];
       i := i+1;
       j := j+1;
    }
    return a;
}

我尝试在 while 循环的不同点放置断言，但没有结果。我认为这是一个读取输入数组的简单程序。在最坏的情况下，i == j。但由于某种我不明白的原因，验证失败了。

任何关于失败原因的见解以及如何继续的可能提示都会有所帮助。请注意，我确实想使用

exists

保留不变式

Answer 1

这似乎是达夫尼应该自己弄清楚的简单不变量或断言，但事实并非如此。

为了帮助 Dafny，您可以在 while 主体中添加

assert a[i] == a[j];

作为第一个语句。