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

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

Дело в том, что после модификации правдаНазначениестек.действительный дает сбой, даже если стек.действительный не знает о правдаНазначение.

assert stack.valid();
truthAssignment[variable] := 1;
assert stack.valid();  // assertion violation
Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
1
0
113
2
Перейти к ответу Данный вопрос помечен как решенный

Ответы 2

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

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

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

но почему изменение одного повлияет на другое? Я несколько раз сталкивался с проблемами равенства между последовательностями, но не так...

Andrici Cezar 15.04.2019 07:22

это не имеет смысла для меня. мы должны спросить Растана.

James Wilcox 15.04.2019 19:55
Ответ принят как подходящий

Причина, по которой Дафни не может проверить утверждение 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?

Andrici Cezar 19.04.2019 10:09

Потому что в утверждении неявно упоминается куча, а ваше задание меняет кучу.

Rustan Leino 23.04.2019 00:56

Другие вопросы по теме