dafny странное поведение без псевдонима памяти - PullRequest
Новая
       115

dafny странное поведение без псевдонима памяти

1 голос
/ 06 августа 2020

У меня есть dafny определенный ADT графа (из этот вопрос SO ), приведенный здесь снова для полноты: 

class Graph
{
    var adjList : seq<seq<int>>;
    constructor (adjListInput : seq<seq<int>>)
        ensures adjList == adjListInput
    {
        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]]);
    var nonRelatedArray := new int[8];
    var i := 0; while (i < 14)
    {
        // nonRelatedArray[3] := 55;
        i := i + 1;
    }
    assert (ValidGraph(G));
}

Если я удалю комментарий к nonRelatedArray по индексу 3, я получаю нарушение утверждения , что немного странно, потому что кажется разумным, что модель памяти сможет определить, что nonRelatedArray (ну) не связано с G.

1 Ответ

1 голос
/ 06 августа 2020

Это можно исправить, добавив modifies nonRelatedArray к l oop. Ключом к этому предложению изменений является то, что в нем не упоминается G. Итак, Дафни знает, что G не будет изменен l oop, поэтому он все равно будет действительным графиком. oop. Если вы не выполняете никаких операций записи в кучу (например, когда вы комментируете запись выше), то Дафни (фактически Boog ie) может автоматически видеть, что вообще ничего не изменилось. Но если вы выполняете какие-либо записи в кучу, предложение Dafny по умолчанию, модифицирует его, внезапно превращается в «все, что окружающей области разрешено изменять». Если вам нужно что-то другое, кроме этих двух значений по умолчанию, вам нужно запросить это явно, указав предложение модифицирует.

...