Дафни: ошибка постусловия в конструкторе - PullRequest
Новая
       70

Дафни: ошибка постусловия в конструкторе

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

Следующий конструктор не работает и не работает на

parent! В Repr

Почему Дафни не может проверить постусловие, этот родитель не является частью Репр набор? 

constructor Init(x: HashObj, parent:Node?)
    ensures Valid() && fresh(Repr - {this, data})
    ensures Contents == {x.get_hash()}
    ensures Repr == {this, data};
    ensures left == null;
    ensures right == null;
    ensures data == x;
    ensures parent != null ==> parent !in Repr;
    ensures this in Repr;
{
    data := x;
    left := null;
    right := null;
    Contents := {x.get_hash()};
    Repr := {this} + {data};
}

1 Ответ

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

Я предполагаю, что HashObj - это trait? (Если это class, то ваш пример проверяет меня.) Проверка не выполняется, потому что проверяющий считает, что x может равняться parent.

Проверяющий должен знать, что Node не является HashObj (если, конечно, ваш класс Node действительно не расширяет HashObj), но это не так. Вы можете зарегистрировать это как проблему на https://github.com/dafny-lang/dafny, чтобы исправить это.

Тем временем вы можете написать предварительное условие, в котором указано, что x и parent разные. Здесь тоже есть морщинка. Вы хотели бы написать 

requires x != parent

, но (если Node действительно не расширяет HashObj) это не проверка типа. Итак, вы хотите преобразовать parent в object?. Нет прямого синтаксиса для такого преобразования, но вы можете сделать это с помощью выражения let: 

requires x != var o: object? := parent; o
...