用 Dafny 证明 BFS 的终止

Question

• 我正在尝试用 dafny 证明 BFS 的一些属性， 但到目前为止，我甚至无法证明终止。
• 算法的进展由以下事实来保证：一旦节点被着色为false（已访问），它将不会再次被着色为true。
• 不过，我很难将这一事实转化为正式的 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

Answer 1

这是一种方法。

关键是引入“尚未着色为假的索引集”的概念。对于这个概念，我使用了一个函数TrueIndices。

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

BFS 方法的开头保持不变：

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。在这种情况下，算法会弹出工作列表的一个元素，然后将所有未访问的邻居标记为已访问。如果没有未访问的邻居，则工作列表的大小会减小。如果有未访问的邻居，则将它们标记为已访问，因此未访问的节点总数减少。

总而言之，要么未访问节点的数量减少（在这种情况下工作列表可能会变长），要么未访问节点的数量保持不变，但工作列表的长度会减少。我们可以通过说循环减少字典顺序中的元组(number of unvisited nodes, length of Q) 来形式化这个推理。

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

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

代码还包含证明减少子句所必需的几个不变量和断言。您可能想在这一点上停下来并尝试自己弄清楚它们，仅从减少子句开始。或者你可以阅读下面的叙述，看看我是怎么想出来的。

---

如果你只添加descend 子句，你会得到两个错误。首先，Dafny 会说它不能证明减少子句减少了。让我们回到那个。第二个错误是内部循环的循环条件中表达式G.adjList[u] 的“索引超出范围”错误。基本上，它不能证明u 在此范围内。哪一种有意义，因为u 只是Q 的一些任意元素，我们还没有给出关于Q 的任何循环不变量。

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

不幸的是，仅添加该行并不能立即解决问题。而且，我们得到一个额外的错误，我们刚刚添加的新循环不变量可能不会由循环维护。为什么这个不变量没有修复错误？问题是，尽管u 被定义为Q[0]，但对Dafny 来说，u 是Q 的一个元素实际上仍然不明显。我们可以通过添加标记为// trigger invariant (1) for u 的断言来解决此问题。

现在让我们尝试证明invariant (1) 被循环保存。问题是有一个没有循环不变量的内部循环。因此，Dafny 对内部循环可能对Q 造成的影响做出了最坏的假设。我们可以通过将相同的不变量复制粘贴到内部循环来解决这个问题，我在上面标记为// invariant (2)。

这修复了外循环的“可能无法保留invariant (1)”错误，但现在我们收到一个新错误，指出invariant (2) 可能无法进入内循环。是什么赋予了？从外部循环的顶部开始，我们所做的就是将Q 的元素出列。我们可以帮助 Dafny 看到出队后的所有元素也是循环顶部原始 Q 的元素。我们使用上面标记为// help Dafny see that dequeueing is ok 的断言来执行此操作。

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

同样，问题在于内部循环。在没有不变量的情况下，Dafny 对color 和Q 可能发生的情况做出最坏的假设。基本上，我们需要找到一种方法来保证，在内循环终止后，元组(TrueIndices(color), |Q|) 与其在外循环顶部的值相比按字典顺序减少了。我们通过在这里说明字典顺序的含义来做到这一点：TrueIndices(color) 变得严格更小，或者在|Q| 变得更小时保持不变。这在上面被声明为// invariant (3)。 （请注意，不幸的是，在元组(a, b) < (c, d) 上进行排序似乎在这里没有做正确的事情。我在幕后看了看，它实际上做了什么很奇怪。不太确定为什么会这样，但就这样吧. 我提交了一个关于这个here的问题。）

添加invariant (3) 会导致关于descue 子句不减少的错误消失，但我们得到最后一个错误，即invariant (3) 可能不会被内部循环保留。这里的问题基本上是在 if 的真正分支中，我们需要帮助 Dafny 意识到 v 是将从 TrueIndices 中删除的索引，我们使用标记为 // help Dafny see that v was newly colored false 的断言来执行此操作。

这样就完成了终止证明！

请注意，正如在复杂的终止参数中经常出现的情况一样，我们必须在此过程中证明其他几个不变量。起初，这可能会让您有些惊讶，因为终止和正确性似乎是独立的。但实际上，这种情况很常见。

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