Дафни провал предварительного условия

Question

• Я пытаюсь запустить dafny проверенную версию 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

Answer 1

Вам просто нужно добавить ensures adjList == adjListInput в конструктор. Поскольку Дафни рассматривает конструктор в основном как метод, и поскольку Дафни анализирует каждый метод изолированно, при анализе main Дафни использует только спецификацию конструктора, а не тело конструктора. Итак, причина сбоя утверждения заключалась в том, что с точки зрения main конструктор устанавливал для поля adjList произвольное значение, которое необязательно соответствовало его аргументу.