愚蠢的前置条件失败答案

【问题标题】：dafny pre-condition failure愚蠢的前置条件失败
【发布时间】：2020-11-25 15:02:05
【问题描述】：

我正在尝试运行经过验证的 BFS 版本（来自 here）
我的输入图非常好，但由于某种原因它未能通过前置条件检查。
这里是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

【问题讨论】：

标签： dafny preconditions

【解决方案1】：

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

【讨论】：