Вызов Dafny может нарушать условие изменения контекста при использовании фабричного шаблона.

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

class Counter {
    var i: int;
    constructor() {
        i := 0;
    }
    method Count()
        modifies this
    {
        i := i + 1;
    }
}

method CounterFactory() returns (r: Counter)
{
    r := new Counter();
}

method Main() {
    var counter := CounterFactory();
    counter.Count(); // <~~ Error: call may violate context's modifies clause
}

Когда я заменяю строку непосредственно над ошибкой на var counter := new Counter();, верификатор не жалуется.


dafny
person Jones    schedule 27.08.2019    source источник

Ответы (1)


arrow_upward
0
arrow_downward

CounterFactory() требуется постусловие, чтобы показать, что возвращаемый объект является новым. Метод работы выглядит так:

method CounterFactory() returns (r: Counter)
    ensures fresh(r)
{
    r := new Counter();
}
person Jones    schedule 27.08.2019