用Dafny证明BFS的终止 [英] Proving termination of BFS with Dafny

问题描述

• 我正尝试通过dafny来证明BFS的某些属性，但到目前为止，我甚至无法证明终止.
• 算法的进展是通过以下事实来保证的:节点一旦被着色为 false (被访问)，它将不被着色为 true 再次.
• 仍然，我很难把这个事实翻译成正式的dafny 减少< something> :

• I'm trying to prove some properties of BFS with dafny, but so far I can't even prove termination.
• The progression of the algorithm is guaranteed by the fact that once a node is colored false (visited) it will not be colored true again.
• Still, I am having a hard time translating this fact to a formal dafny decreases <something>:

class Graph {
    var adjList : seq<seq<int>>;
}
method BFS(G : Graph, s : int) returns (d : array<int>)
    requires 0 <= s < |G.adjList|
    requires forall u :: 0 <= u < |G.adjList| ==> forall v   :: 0 <= v <     |G.adjList[u]| ==> 0 <= G.adjList[u][v] < |G.adjList|
    requires forall u :: 0 <= u < |G.adjList| ==> forall v,w :: 0 <= v < w < |G.adjList[u]| ==> G.adjList[u][v] != G.adjList[u][w] 
{
    var i := 0;
    var j := 0;
    var u : int;
    var Q : seq<int>;
    var iterations := G.adjList[0];
    var n := |G.adjList|;
    var color : array<bool>;

    color := new bool[n];
    d     := new int [n];

    i := 0; while (i < n)
    {
        color[i] := true;
        d[i] := -1;
        i := i + 1;
    }

    Q := [s];
    while (Q != [])
    {        
        // u <- Dequeue(Q)
        u := Q[0]; Q := Q[1..];
        
        // foreach v in adjList[u]
        i := 0; while (i < |G.adjList[u]|)
        {
            var v := G.adjList[u][i];
            if (color[v])
            {
                color[v] := false;
                d[v]     := d[u] + 1;
                Q        := Q + [v];
            }
            i := i + 1;
        }
    }
}

我收到的错误消息是:

cannot prove termination; try supplying a decreases clause for the loop

推荐答案

这是一种实现方法.

关键是要引入尚未被着色为假的索引集"的概念.对于这个概念，我使用一个函数 TrueIndices .

The key is to introduce the concept of "the set of indices that have not yet been colored false". For this concept, I use a function TrueIndices.

function TrueIndices(a: array<bool>): set<int>
  reads a
{
  set i | 0 <= i < a.Length && a[i] 
}

BFS 方法的开头保持不变:

The beginning of the BFS method remains unchanged:

method BFS(G : Graph, s : int) returns (d : array<int>)
    requires 0 <= s < |G.adjList|
    requires forall u :: 0 <= u < |G.adjList| ==>
        forall v :: 0 <= v < |G.adjList[u]| ==> 0 <= G.adjList[u][v] < |G.adjList|
    requires forall u :: 0 <= u < |G.adjList| ==>
        forall v,w :: 0 <= v < w < |G.adjList[u]| ==> G.adjList[u][v] != G.adjList[u][w] 
{
    var i := 0;
    var j := 0;
    var u : int;
    var Q : seq<int>;
    var iterations := G.adjList[0];
    var n := |G.adjList|;
    var color : array<bool>;

    color := new bool[n];
    d     := new int [n];

    i := 0; while (i < n)
    {
        color[i] := true;
        d[i] := -1;
        i := i + 1;
    }

该实现使用工作表 Q .在这种情况下，该算法会弹出工作清单的一个元素，然后将所有未访问的邻居标记为已访问.如果没有未访问的邻居，则工作列表的大小将减小.如果有未访问的邻居，则会将其标记为已访问，因此未访问的节点总数会减少.

The implementation uses a worklist Q. In this case, the algorithm pops an element of the worklist, and then marks all unvisited neighbors as visited. If there are no unvisited neighbors, then the size of the worklist decreases. If there are unvisited neighbors, then they get marked visited, so the total number of unvisited nodes decreases.

总而言之，要么未访问节点的数量减少(在这种情况下，工作列表可能会更长)，要么未访问节点的数量保持不变，但工作列表的长度减少.我们可以说这种循环形式化，就是说该循环减少了字典顺序中的元组(未访问的节点数，Q的长度).

To sum up, either the number of unvisited nodes decreases (in which case the worklist might get longer), or the number of unvisited nodes remains the same, but the length of the worklist decreases. We can formalize this reasoning by saying that the loop decreases the tuple (number of unvisited nodes, length of Q) in the lexicographic ordering.

这正是下面的减少子句中编码的内容.

This is exactly what is encoded in the decreases clause below.

    Q := [s];
    while (Q != [])
      decreases TrueIndices(color), |Q|
      invariant forall x | x in Q :: 0 <= x < |G.adjList|  // invariant (1)
    {        
        ghost var top_of_loop_indices := TrueIndices(color);
        ghost var top_of_loop_Q := Q;

        // u <- Dequeue(Q)
        u := Q[0]; Q := Q[1..];
        assert u in top_of_loop_Q;  // trigger invariant (1) for u

        // help Dafny see that dequeueing is ok
        assert forall x | x in Q :: x in top_of_loop_Q;

        // foreach v in adjList[u]
        i := 0; while i < |G.adjList[u]|
          invariant forall x | x in Q :: 0 <= x < |G.adjList|  // invariant (2)
          invariant  // invariant (3)
            || TrueIndices(color) < top_of_loop_indices
            || (TrueIndices(color) == top_of_loop_indices && |Q| < |top_of_loop_Q|)
        {
            var v := G.adjList[u][i];
            if (color[v])
            {
                // help Dafny see that v was newly colored false
                assert v in TrueIndices(color);
                color[v] := false;
                d[v]     := d[u] + 1;
                Q        := Q + [v];
            }
            i := i + 1;
        }
    }
}

该代码还包含一些不可变和断言，这是证明减少子句所必需的.您可能想停止在这一点上，并尝试自己解决问题，仅从减少子句开始.或者，您可以阅读下面的叙述以了解我的想法.

The code also contains several invariants and assertions that are necessary to prove the decreases clause. You might like to stop at this point and try to figure them out for yourself, starting only from the decreases clause. Or you can read the narrative below to see how I figured it out.

如果仅添加减少子句，则会出现两个错误.首先，达夫尼将说无法证明减少条款减少了.让我们回到这一点.第二个错误是索引超出范围".内部循环的循环条件中，表达式 G.adjList [u] 上的错误.基本上，它不能证明 u 在这里是有界的.哪种方法有意义，因为 u 只是 Q 的任意元素，而且我们还没有给出关于 Q 的任何循环不变式.

If you just add the decreases clause, you will get two errors. First, Dafny will say that it cannot prove that the decreases clause decreases. Let's come back to that. The second error is an "index out of range" error on the expression G.adjList[u] in the loop condition of the inner loop. Basically, it cannot prove that u is in bounds here. Which kind of makes sense, because u is just some arbitrary element of Q, and we haven't given any loop invariants about Q yet.

要解决此问题，我们需要说 Q 的每个元素都是对 G.adjList 的有效索引.这由上面标记为//invariant(1)的行表示.

To fix this, we need to say that every element of Q is a valid index into G.adjList. This is stated by the line marked // invariant (1) above.

不幸的是，仅添加该行并不能立即解决问题.而且，我们还收到另一个错误，即刚才添加的新循环不变式可能无法由该循环维护.为什么这个不变式不能解决错误?问题在于，即使 u 被定义为，对于Dafny来说， u 实际上是 Q 的元素实际上仍然不明显.Q [0] .我们可以通过添加标记为//的u触发不变式(1)的断言来解决此问题.

Unfortunately, adding just that line does not immediately fix the problem. And, we get an additional error that the new loop invariant we just added might not be maintained by the loop. Why didn't this invariant fix the error? The problem is that it's actually still not obvious to Dafny that u is an element of Q, even though u is defined to be Q[0]. We can fix this by adding the assertion marked // trigger invariant (1) for u.

现在让我们尝试证明循环保留了不变式(1).问题是存在一个没有循环不变性的内部循环.因此，达夫妮(Dafny)对内循环可能对 Q 做些什么做出最坏的假设.我们可以通过将相同的不变式复制粘贴到内部循环中来解决此问题，我在上面将其标记为//不变式(2).

Now let's try to prove that invariant (1) is preserved by the loop. The problem is that there is an inner loop with no loop invariants yet. So Dafny makes worst case assumptions about what the inner loop might do to Q. We can fix this by copy-pasting the same invariant to the inner loop, which I marked as // invariant (2) above.

解决了外循环的可能不会保留不变式(1)"的问题.错误，但现在我们收到一个新错误，说不变式(2)可能在进入内部循环时不成立.是什么赋予了?自外部循环的顶部以来，我们所做的所有工作都是使 Q 的元素出队.我们可以帮助Dafny在循环顶部看到出队后的所有元素也是原始 Q 的元素.我们使用标记为//的断言来执行此操作，帮助Dafny确认上面的出队是可以的.

That fixes the outer loop's "might not preserve invariant (1)" error, but now we get a new error saying that invariant (2) might not hold on entry to the inner loop. What gives? All we've done since the top of the outer loop is dequeue an element of Q. We can help Dafny see that all elements after dequeueing were also elements of the original Q at the top of the loop. We do this using the assertion marked // help Dafny see that dequeueing is ok above.

好的，这完成了不变式(1)的证明.现在，让我们修复剩余的错误，即减少子句可能不会减少.

Ok, that completes the proof of invariant (1). Now let's fix the remaining error saying that the decreases clause might not decrease.

同样，问题出在内部循环上.在没有不变性的情况下，Dafny对 color 和 Q 可能发生的情况做出最坏的假设.基本上，我们需要找到一种方法来确保在内部循环终止之后，元组(TrueIndices(color)，| Q |)与在外部顶部的值相比在字典上有所减少环形.我们通过在这里阐明词典顺序的含义来做到这一点: TrueIndices(color)严格变小，或者当 | Q | 变小时，它保持不变.上面表示为//不变量(3).(请注意，不幸的是，在元组(a，b)<(c，d)上排序似乎在这里做不正确.很奇怪.不是很确定为什么会这样，但是就这样.我对此提交了一个问题

Again, the problem is the inner loop. In the absence of invariants, Dafny makes worst case assumptions about what might happen to color and Q. Basically, we need to find a way to guarantee that, after the inner loop terminates, the tuple (TrueIndices(color), |Q|) has lexicographically decreased compared to its value at the top of the outer loop. We do this by spelling out what lexicographic ordering means here: either TrueIndices(color) gets strictly smaller, or it stays the same while |Q| gets smaller. This is stated as // invariant (3) above. (Note that, unfortunately, ordering on tuples (a, b) < (c, d) does not appear to do the right thing here. I looked under the covers, and what it actually does is pretty weird. Not really sure why it is this way, but so be it. I filed an issue about this here.)

添加不变式(3)导致有关reduces子句的错误不会减少，但是我们得到了最后一个错误，即不变式(3)可能不能被内部循环保留.这里的问题基本上是，在if的真实分支内，我们需要帮助Dafny意识到 v 是要从 TrueIndices 中删除的索引，我们这样做断言标记为//，帮助Dafny看到v的颜色被重新设置为假.

Adding invariant (3) causes the error about the decreases clause not decreasing to go away, but we get one last error, which is that invariant (3) might not be preserved by the inner loop. The problem here is basically that inside the true branch of the if, we need to help Dafny realize that v is the index that is going to be removed from TrueIndices we do this with the assertion marked // help Dafny see that v was newly colored false.

这完成了终止证明！

请注意，就像复杂终止参数中经常出现的那样，我们必须在此过程中证明其他几个不变式.刚开始时，这可能会让您感到有些惊讶，因为终止和正确性似乎是相互独立的.但是实际上，这很普遍.

Note that, as is often the case in sophisticated termination arguments, we had to prove several other invariants along the way. This might be somewhat surprising to you at first, since it might seem like termination and correctness would be independent. But in fact, this is quite common.

当然，要实际证明 BFS 的功能正确性，还需要更多不变性.我还没有尝试过，但我希望你能！

Of course, actually proving functional correctness of BFS will require yet more invariants. I haven't tried it, but I hope you will!

这篇关于用Dafny证明BFS的终止的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！