dafny断言很难解释

Question

我试图证明一种确定是否大小为n的序列是0,1,...,n-1的排列。我设法证明，只要方法返回true，那么该序列的确是有效置换。尽管如此，证明相反的情况（对我而言）要困难得多。我认为我有正确的循环不变量和触发器，但是Dafny触发了我无法理解的断言错误。这是permalink，这是完整性代码：

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;
}