愚蠢的先决条件失败

Question

我正在尝试运行一个愚蠢的 BFS 验证版本（来自）
我的输入图非常好，但由于某种原因未能通过先决条件检查。
这是permalink
为了完整起见，这里是图表定义 + 有效性条件

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

dafny 的回复是 Error: assertion violation

Answer 1

你只需要在构造函数中添加ensures adjList == adjListInput。由于 Dafny 基本上将构造函数视为方法，并且由于 Dafny 孤立地分析每个方法，因此当 Dafny 分析 main 时，它仅使用构造函数的规范，而不使用构造函数的主体。所以断言失败的原因是因为从 main 的角度来看，构造函数将字段 adjList 设置为一个不一定与其参数相对应的任意值。

愚蠢的先决条件失败

dafny pre-condition failure

dafny

preconditions