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

Question

我正在尝试创建一个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;
}
}`

Answer 1

"invariant not hold on entry"错误是针对声明的invariant

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]) // (**)

即CCD_ 5告诉您在第一个CCD_。条件(*(表示a[i]，而(**(不表示a[i]。

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

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

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