Dafny断言失败很难解释

Question

我试图证明一个确定是否大小n序列是0,1,...,n-1的排列。我设法证明，每当该方法返回true时，序列确实是一个有效的排列。尽管如此，证明相反的情况要困难得多(对我来说(。我认为我有正确的循环不变量和触发器，但 Dafny 触发了一个我无法理解的断言错误。这是永久链接，这是完整性的代码：

method perm_imperative(s: seq<int>) returns (status : bool)
    requires |s| > 0
    ensures (status == true ) ==> (forall i    :: 0 <= i      < |s| ==> 0 <= s[i] < |s|)
    ensures (status == true ) ==> (forall i, j :: 0 <= i <  j < |s| ==> (s[i] != s[j]))
    ensures (status == false) ==> (exists i, j :: 0 <= i <= j < |s| &&  (
        (s[i] <   0  ) ||
        (s[i] >= |s| ) ||
        (s[i] == s[j]  && (i != j))))
{
    var i := 0;
    var used := new int[|s|];
    while (i < |s|)
        invariant 0 <= i <= |s|
        invariant forall k :: 0 <= k < i ==> used[k] == -1; 
    {
        used[i] := -1;
        i := i + 1;
    }
    assert (forall k :: 0 <= k < |s| ==> used[k] == -1);
    i := 0;
    while (i < |s|)
        invariant 0 <= i <= |s|
        invariant forall k    :: 0 <= k < i     ==> 0 <= s[k]       < |s|
        invariant forall k    :: 0 <= k < i     ==> 0 <= used[s[k]] <  i
        invariant forall k, m :: 0 <= k < m < i ==> s[k] != s[m]
        invariant forall k    :: 0 <= k     < i ==> used[s[k]] == k
        invariant forall k    :: 0 <= k     < i ==> s[used[s[k]]] == s[k]
        invariant forall k, m :: 0 <= k < m < i ==> used[s[k]] != used[s[m]]
        invariant forall k    :: 0 <= k < |s|   ==> (0 <= used[k] < i) || (used[k] == -1)
    {
        if (s[i] < 0)
        {
            // assert (s[i] < 0);
            return false;
        }
        else if (s[i] >= |s|)
        {
            // assert (s[i] >= |s|);
            return false;
        }
        else if (used[s[i]] != -1)
        {
            assert (0 <= s[i]       < |s|);
            assert (0 <= used[s[i]] <  i );
            //////////////////
            //              //
            // ASSERT ERROR //
            //       |      //
            //       V      //
            //////////////////
            assert (s[used[s[i]]] == s[i]);
            return false;
        }
        assert (used[s[i]] == -1);
        used[s[i]] := i;
        i := i + 1;
    }
    return true;
}

Answer 1

如果添加以下循环不变量，则证明通过：

invariant forall n | 0 <= n < |s| :: used[n] != -1 ==> exists k | 0 <= k < i :: s[k] == n

这基本上表明used正确记录了在以前的迭代中s中看到的所有数字。

如果添加此循环不变量，则可以删除前面的四个循环不变量，以及 while 循环主体中的所有断言：

method perm_imperative(s: seq<int>) returns (status : bool)
    requires |s| > 0
    ensures (status == true ) ==> (forall i    :: 0 <= i      < |s| ==> 0 <= s[i] < |s|)
    ensures (status == true ) ==> (forall i, j :: 0 <= i <  j < |s| ==> (s[i] != s[j]))
    ensures (status == false) ==> (exists i, j :: 0 <= i <= j < |s| &&  (
        (s[i] <   0  ) ||
        (s[i] >= |s| ) ||
        (s[i] == s[j]  && (i != j))))
{
    var i := 0;
    var used := new int[|s|];
    while (i < |s|)
        invariant 0 <= i <= |s|
        invariant forall k :: 0 <= k < i ==> used[k] == -1; 
    {
        used[i] := -1;
        i := i + 1;
    }
    assert (forall k :: 0 <= k < |s| ==> used[k] == -1);
    i := 0;
    while (i < |s|)
        invariant 0 <= i <= |s|
        invariant forall k    :: 0 <= k < i     ==> 0 <= s[k]       < |s|
        invariant forall k    :: 0 <= k < i     ==> 0 <= used[s[k]] <  i
        invariant forall k, m :: 0 <= k < m < i ==> s[k] != s[m]
        // invariant forall k    :: 0 <= k     < i ==> used[s[k]] == k
        // invariant forall k    :: 0 <= k     < i ==> s[used[s[k]]] == s[k]
        // invariant forall k, m :: 0 <= k < m < i ==> used[s[k]] != used[s[m]]
        // invariant forall k    :: 0 <= k < |s|   ==> (0 <= used[k] < i) || (used[k] == -1)
        invariant forall n | 0 <= n < |s| :: used[n] != -1 ==> exists k | 0 <= k < i :: s[k] == n
    {
        if (s[i] < 0)
        {
            // assert (s[i] < 0);
            return false;
        }
        else if (s[i] >= |s|)
        {
            // assert (s[i] >= |s|);
            return false;
        }
        else if (used[s[i]] != -1)
        {
            // assert (0 <= s[i]       < |s|);
            // assert (0 <= used[s[i]] <  i );
            // assert (s[used[s[i]]] == s[i]);
            return false;
        }
        // assert (used[s[i]] == -1);
        used[s[i]] := i;
        i := i + 1;
    }
    return true;
}