Я столкнулся со странной проблемой в Дафни. Я пытался максимально извлечь его здесь: https://rise4fun.com/Dafny/F7sK
Дело в том, что после модификации правдаНазначениестек.действительный дает сбой, даже если стек.действительный не знает о правдаНазначение.
assert stack.valid();
truthAssignment[variable] := 1;
assert stack.valid(); // assertion violation
Следующее подтверждает для меня:
assert stack.valid();
ghost var old_stack := stack.stack[..];
truthAssignment[variable] := 1;
assert stack.stack[..] == old_stack;
assert stack.valid();
Я действительно не понимаю, почему это работает, но это подпадает под общую категорию «экстенсиональное равенство последовательностей сложно для Дафни».
это не имеет смысла для меня. мы должны спросить Растана.
Причина, по которой Дафни не может проверить утверждение 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
после обновления работает и в этом случае.
Рустан
Но почему Дафни снова проверяет утверждение, если stack.valid не связан с trueAssignment?
Потому что в утверждении неявно упоминается куча, а ваше задание меняет кучу.
но почему изменение одного повлияет на другое? Я несколько раз сталкивался с проблемами равенства между последовательностями, но не так...