Dafny. Другой случай вызова может нарушить условие модификации контекста

Question

Я прочитал много вопросов здесь и в вики по этому поводу, но я не смог решить этот случай "вызов может нарушить условие изменения контекста".Не могли бы вы помочь мне?Я пытаюсь отправить экземпляр проблемы «решателю» из метода main, и когда я вызываю метод 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();
}

Answer 1

Вам не хватает постусловия

ensures f == f'

в конструкторе для класса Solver.

(Так как конструкторы являются методами, Дафни не "заглядывает внутрь" своих тел при рассуждениио других методах, поэтому вам нужно это постусловие, чтобы выставить тело.)