Dafny - 嵌套循环的循环不变性。

问题描述 投票:0回答:1

我试图创建一个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个回答
0
投票

不变数在输入时不成立 "的错误是针对声明的不变数的

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

的内部循环。在进入该循环时。j0所以进入内循环时需要保持的条件是

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])

然后,在内循环之后,更新 r 使用您计算的 s.

© www.soinside.com 2019 - 2024. All rights reserved.