Dafny - 嵌套循环的循环不变性
Dafny - Loop invariant for nested loops
我正在尝试创建一个 Dafny 程序,当且仅当 A 不包含重复项时,该程序 returns 为真。
这是我目前所拥有的,但是不变量 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;
}
}`
"invariant doesn't hold on entry" 错误是针对声明的不变量
r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i])
内循环。进入that循环时,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
。
我正在尝试创建一个 Dafny 程序,当且仅当 A 不包含重复项时,该程序 returns 为真。
这是我目前所拥有的,但是不变量 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;
}
}`
"invariant doesn't hold on entry" 错误是针对声明的不变量
r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i])
内循环。进入that循环时,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
。