1

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

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

1 回答 1

0

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

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;
}
于 2019-10-03T01:53:58.903 回答