Я прочитал много вопросов здесь и в вики по этому поводу, но я не смог решить этот случай «вызов может нарушить условие изменения контекста». Не могли бы вы помочь мне? Я пытаюсь отправить экземпляр проблемы в «решатель» из основного метода, и когда я вызываю метод solve()
, я получаю эту ошибку, и я не понимаю, почему. https://rise4fun.com/Dafny/53q6
class Stack {
var x : array<int>;
constructor()
ensures fresh(x);
{
x := new int[10];
}
}
class Formula {
var stack : Stack;
constructor()
ensures fresh(stack);
ensures fresh(stack.x);
{
stack := new Stack();
}
}
class Solver {
var f : Formula;
constructor(f' : Formula)
{
this.f := f';
}
method solve()
modifies f.stack;
ensures old(f.stack.x) == f.stack.x;
{}
}
method Main() {
var f := new Formula();
var a := new Solver(f);
assert fresh(f);
assert fresh(f.stack);
assert fresh(f.stack.x);
assert fresh(a);
a.solve();
}
Вам не хватает постусловия
ensures f == f'
в конструкторе класса Solver
.
(Поскольку конструкторы являются методами, Дафни не «заглядывает внутрь» их тел, рассуждая о других методах, поэтому вам нужно это постусловие, чтобы раскрыть тело.)