Сбой утверждения после изменения другого массива в Dafny

Question

Я столкнулся со странной проблемой в Дафни. Я попытался извлечь его как можно больше здесь: https://rise4fun.com/Dafny/F7sK

Дело в том, что после модификации trueAssignment , stack.valid происходит сбой, даже если stack.valid не знает о trueAssignment .

assert stack.valid();
truthAssignment[variable] := 1;
assert stack.valid();  // assertion violation

Answer 1

Причина, по которой Дафни не может проверить утверждение assert stack.valid(); - последний конъюнкт в теле valid():

(forall c :: c in contents ==>
  exists i,j :: 0 <= i < stack.Length 
             && 0 <= j < |stack[i]| 
             && stack[i][j] == c)

Он имеет форму forall ... exists ..., и доказательство такого условия как инвариантного трудно для верификатора. Как только вы выяснили, что это часть valid(), которую верификатор не может доказать (что вы можете сделать, например, вручную вставив определение valid() вместо вашего утверждения), тогда решение состоит в том, чтобы дать верификатор некоторая помощь.

Когда верификатор - или человек, в этом отношении - пытается доказать что-то для формы forall c :: P(c), тогда он составляет произвольный c, а затем пытается доказать "P(c)" для него , (Логики называют это правило «универсальным введением».) Легко. Затем, чтобы доказать что-то в форме exists i,j :: Q(i,j), проверяющий ищет свидетеля "Q(i,j)". (Это называется «экзистенциальным введением».) Здесь верификатор не особенно креативен и часто нуждается в помощи. Иногда вам нужно выяснить некоторые i и j самостоятельно, а затем утверждать Q(i,j). В других случаях достаточно просто упомянуть какой-то компонент необходимого Q(i,j), и верификатор тогда выяснит остальное. Именно то, что нужно сделать, может быть методом проб и ошибок.

Что делает вышеперечисленное лекарство Джеймса тем, что в нем упоминается stack.stack[..] после обновления truthAssignment[variable] := 1;. Это щекочет верификатор таким образом, чтобы он мог видеть свет. Просто написание тривиально доказанного утверждения:

assert 0 <= |stack.stack[..]|;  // mentioning stack.stack[..] helps the verifier in the next line

после обновления также работает в этом случае.

Rustan

Answer 2

Следующее подтверждает для меня:

assert stack.valid();
ghost var old_stack := stack.stack[..];
truthAssignment[variable] := 1;
assert stack.stack[..] == old_stack;
assert stack.valid();

Я не очень понимаю, почему это работает, но оно подпадает под общую категорию "экстренное равенство для последовательностей трудно для Дафни".