Дафни: метод должен обеспечивать такое же или более разрешающее предварительное условие, чем в его родительском признаке - PullRequest
Новая
       59

Дафни: метод должен обеспечивать такое же или более разрешающее предварительное условие, чем в его родительском признаке

0 голосов
/ 25 мая 2020

В настоящее время я пытаюсь построить трейт для BinaryTree в Dafny. При реализации метода Insert в классе возникает следующая ошибка:

метод должен предоставлять такое же или более разрешающее предварительное условие, чем в его родительской характеристике

Почему эта ошибка возникает, даже если для метода в трейте и в классе существуют одинаковые предварительные условия?

Это черта: 

trait DataStorage {
    ghost var Contents: set<int>
    ghost var Repr: set<object>

    method Insert(val: int)
        modifies this, Repr
        requires Valid()
        ensures Valid() && fresh(Repr - old(Repr))
        ensures Contents == old(Contents) + {val}

    predicate Valid()
        reads this, Repr

    (...)
}

Это соответствующая реализация 

class BinaryTree extends DataStorage {

    var root: Node?;

    predicate Valid()
        reads this, Repr
    {
        this in Repr &&
        (root == null ==> Contents == {}) &&
        (root != null ==>
        root in Repr && root.Repr <= Repr && this !in root.Repr &&
        root.Valid() &&
        Contents == root.Contents)
    }


    method Insert(val: int)
        requires Valid()
        modifies Repr
        ensures Valid() && fresh(Repr - old(Repr))
        ensures Contents == old(Contents) + {val}
    {
        var n := insert_helper(root, val);
        root := n;
        Contents := root.Contents;
        Repr := root.Repr + {this};
    }

    (...)
}
...