Dafny - 嵌套循环的循环不变量答案

【问题标题】：Dafny - Loop invariant for nested loopsDafny - 嵌套循环的循环不变量
【发布时间】：2020-08-05 13:08:05
【问题描述】：

我正在尝试创建一个 Dafny 程序，当且仅当 A 不包含重复项时才返回 true。

这是我到目前为止所拥有的，但是不变量 invariant r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i]); 表示它不会保留进入。

关于我做错了什么有什么建议吗？

`method CheckArr1(A: array<int>) returns (r: bool)
requires A.Length > 0
ensures r <==> (forall i, j :: 0 <= i < A.Length && 0 <= j < A.Length && i != j ==> A[i] != A[j]);
{
    var i := 0;
    r := true;
    while i < A.Length 
    decreases A.Length - i;
    invariant i <= A.Length;
    invariant r <==> (forall x, y :: 0 <= x < i && 0 <= y < i && x != y ==> A[x] != A[y]);
    {
        var j := 0;
        while j < i
        decreases i - j;
        invariant j <= i;
        invariant r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i]);
        {
            r := (r && (A[j] != A[i]));
            j := j + 1;
        }
        i := i + 1;
    }
}`

【问题讨论】：

标签： dafny

【解决方案1】：

“invariant doesn't hold on entry”错误是针对声明的不变量

r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i])

的内部循环。在进入那个循环时，j 是0，所以进入内循环需要保持的条件是

r <==> (0 <= 0 < i && 0 != i ==> A[0] != A[i])

我们可以简化为

r <==> (0 < i ==> A[0] != A[i])           // (*)

没有理由相信r 会在进入内部循环时保持这个值。你在外循环体内所知道的就是

r <==> (forall x, y :: 0 <= x < i && 0 <= y < i && x != y ==> A[x] != A[y]) // (**)

这表示r 告诉您在第一个i 元素中是否有任何重复项。条件 (*) 表示有关 a[i] 的内容，而 (**) 未表示有关 a[i] 的任何内容。

在您当前的程序中，如果您更改内部循环以使用不同的变量（例如 s）来实现您给出的不变量，会更容易。也就是说，使用不变量

s <==> (forall j :: 0 <= j < i ==> A[j] != A[i])

然后，在内循环之后，使用您为s 计算的值更新r。

【讨论】：