dafny - 愚蠢的前置条件失败

Question

• 我正在尝试运行一个经过验证的 BFS 版本（从这里开始）
• 我的输入图非常好，但由于某种原因它未能通过前置条件检查。
• 这是永久链接
• 为了自我完整性，这里是图定义+有效性条件

class Graph
{
    var adjList : seq<seq<int>>;
    constructor (adjListInput : seq<seq<int>>)
    {
        adjList := adjListInput;
    }
}
function ValidGraph(G : Graph) : bool
    reads G
{
    (forall u :: 0 <= u < |G.adjList| ==> forall v   :: 0 <= v <     |G.adjList[u]| ==> 0 <= G.adjList[u][v] < |G.adjList|) &&
    (forall u :: 0 <= u < |G.adjList| ==> forall v,w :: 0 <= v < w < |G.adjList[u]| ==> G.adjList[u][v] != G.adjList[u][w])
}
method main()
{
    var G : Graph := new Graph([[1,2],[0,2],[0,1]]);
    assert (ValidGraph(G));
}

• 达芙妮的回应是Error: assertion violation

标签： dafnypreconditions

Answer 1

您只需要添加ensures adjList == adjListInput到构造函数。因为 Dafny 基本上把构造函数当作方法来对待，并且因为 Dafny 对每个方法进行单独分析，所以 Dafny 在分析main时只使用构造函数的规范，而不是构造函数的主体。所以断言失败的原因是因为从 的角度来看main，构造函数将字段设置adjList为一个不一定对应于其参数的任意值。