Дафни не может доказать простой квантификатор существования

Это может быть очень глупый вопрос, но вот:

Почему Дафни может очень это:

var arr := new int[2];
arr[0], arr[1] := -1, -2;
assert exists k :: 0 <= k < arr.Length && arr[k] < 0;

Но не это:

var arr := new int[2];
arr[0], arr[1] := -1, 2;
assert exists k :: 0 <= k < arr.Length && arr[k] < 0;

Я проследил ошибку в моей большей программе до этого. Я уверен, что это что-то незначительное, что я упустил из виду, но я был бы признателен за помощь!

Как настроить Tailwind CSS с React.js и Next.js?
Как настроить Tailwind CSS с React.js и Next.js?
Tailwind CSS - единственный фреймворк, который, как я убедился, масштабируется в больших командах. Он легко настраивается, адаптируется к любому...
LeetCode запись решения 2536. Увеличение подматриц на единицу
LeetCode запись решения 2536. Увеличение подматриц на единицу
Увеличение подматриц на единицу - LeetCode
Переключение светлых/темных тем
Переключение светлых/темных тем
В Microsoft Training - Guided Project - Build a simple website with web pages, CSS files and JavaScript files, мы объясняем, как CSS можно...
Отношения &quot;многие ко многим&quot; в Laravel с методами присоединения и отсоединения
Отношения &quot;многие ко многим&quot; в Laravel с методами присоединения и отсоединения
Отношения "многие ко многим" в Laravel могут быть немного сложными, но с помощью Eloquent ORM и его моделей мы можем сделать это с легкостью. В этой...
В PHP
В PHP
В большой кодовой базе с множеством различных компонентов классы, функции и константы могут иметь одинаковые имена. Это может привести к путанице и...
Карта дорог Беладжар PHP Laravel
Карта дорог Беладжар PHP Laravel
Laravel - это PHP-фреймворк, разработанный для облегчения разработки веб-приложений. Laravel предоставляет различные функции, упрощающие разработку...
2
0
85
2
Перейти к ответу Данный вопрос помечен как решенный

Ответы 2

Интересный вопрос. Я не уверен! Может быть, кто-то еще сможет присоединиться к более глубокому расследованию.

Позвольте мне только упомянуть, что эта проблема связана с триггерами. Каждый раз, когда вы просите Дафни доказать существование, вы должны понимать, что он (и базовый решатель Z3) использует синтаксическую эвристику. Он смотрит на тело квантификатора и пытается найти «триггер» или шаблон. После выбора триггера он будет угадывать только те значения k, которые соответствуют триггеру.

В вашем конкретном примере триггером является arr[k]. Таким образом, Дафни будет пытаться угадать значения k только там, где arr[k] уже упоминается в другом месте программы.

Также важно понимать, что массивы размещаются в куче, и пункт «упомянутый в другом месте программы» в основном относится к текущей куче. Программа упоминает arr[0] и arr[1], но они упоминаются в предыдущей куче перед оператором присваивания в строке 2.

Все это говорит о том, что я на самом деле больше удивлен тем, что Дафни может доказать утверждение в вашем первом примере, чем тем, что он не может доказать второй.

Наконец, позвольте мне отметить, что как только вы поймете, что триггеры — это то, как Дафни понимает квантификаторы, легко вручную уговорить Дафни доказать второе утверждение: просто упомяните arr[k] для значения k, которое, как вы знаете, является правильным. Другими словами, вставьте эту строку в вашу программу перед существующим утверждением:

assert arr[0] < 0;

Обратите внимание, что на самом деле не важно, что мы утверждаем, что arr[0] меньше 0. Важно то, что мы вообще упоминаем arr[0]. Вместо этого мы могли бы сказать что-нибудь глупое об этом, пока упоминаем об этом.

Это очень интересно! Я также заметил, что он уже работает с утверждениями. Дело в том, что я делаю это для университетского задания, где мне не разрешено добавлять утверждения (другой пример): D Так что мне придется подумать об этом еще немного. Спасибо!

arn 21.11.2022 07:49

+1. Я начал редактировать ваш ответ, но он стал слишком длинным, поэтому я сделал отдельный ответ. Проблема в том, что второе обновление кучи скрывает первое (поэтому у нас есть основной термин и, следовательно, экземпляр только для arr[1], а не arr[0]).

Clément 29.11.2022 19:19
Ответ принят как подходящий

Эта тонкая проблема связана с порядком, в котором обрабатываются обновления кучи. Во-первых, давайте упростим пример, потому что он ничего не говорит о положительных и отрицательных числах.

type T
predicate P(t: T)

method ThisFails(t0: T, yes: T, no: T) requires P(yes) && !P(no) {
  var arr := new T[2](_ => t0);
  arr[0] := yes;
  arr[1] := no;
  assert exists k :: 0 <= k < arr.Length && P(arr[k]); // FAILS [:(]
}

Переключение двух модификаций массива устраняет проблему:

type T
predicate P(t: T)

method ThisFails(t0: T, yes: T, no: T) requires P(yes) && !P(no) {
  var arr := new T[2](_ => t0);
  arr[1] := no;  // Different order
  arr[0] := yes; // Different order
  assert exists k :: 0 <= k < arr.Length && P(arr[k]); // SUCCEEDS [?!]
}

Почему эти примеры ведут себя по-разному?

Чтобы понять, что происходит, нужно подумать о том, как arr[idx] := value] влияет на состояние проверки. Когда вы присваиваете значение массиву, Дафни узнает, что:

  • Массив изменился
  • Позиция idx сопоставляется с value в новом массиве
  • Другие позиции между старым и новым массивом неизменны.

Итак, после двух присваиваний в первом (неработающем) примере кода выше мы имеем

  • Массив изменился
  • Позиция 0 сопоставляется с yes в промежуточном массиве
  • Позиция 1 сопоставляется с no в конечном массиве

Напротив, после двух присваиваний во втором (рабочем) примере кода выше мы имеем:

  • Массив изменился
  • Позиция 1 сопоставляется с no в промежуточном массиве
  • Позиция 0 сопоставляется с yes в конечном массиве

Обратите внимание, какой факт говорит о промежуточном массиве, а какой факт говорит о конечном массиве. В сломанном примере мы знаем arr[0] == yes в промежуточном массиве. В рабочем примере мы знаем arr[0] == yes в конечном массиве.

Конечно, мы можем доказать, что в конечном массиве есть arr[0] == yes, но мы не знаем этого по умолчанию во втором (сломанном) сломанном примере.

Почему это важно?

Доказательство квантора проходит следующим образом:

  1. Отрицайте утверждение: оно становится forall k | 0 <= k < arr.Length :: !P(arr[k])
  2. Найдите противоречие, создав экземпляр квантификатора.

Если вы наведете курсор на квантификатор, вы увидите Selected triggers: {arr[k]} Это означает, что Дафни будет «учиться» !P(arr[k]) каждый раз, когда она уже знает что-то о arr[k] для некоторых k.

Важно отметить, что квантификатор относится к конечному состоянию массива! Таким образом, факты о промежуточном состоянии массива не используются.

В разбитом примере выше мы узнаем о конечном массиве следующее, чего недостаточно, чтобы вывести противоречие и завершить доказательство.

  • arr[1] == no (из последнего задания, отсюда !P(arr[1]))
  • !P(arr[1]) (из квантификатора)

В рабочем примере выше мы узнаем о конечном массиве следующее, чего достаточно, чтобы вывести противоречие и завершить доказательство.

  • arr[0] == yes (из последнего задания, отсюда P(arr[0]))
  • !P(arr[0]) (из квантификатора)

В неработающем случае проблема может быть решена утверждением assert arr[0] == yes;, что легко доказуемо и дает нам тот факт, который нам нужен в отношении конечного массива.

Заключительные замечания

Мы можем сделать промежуточные состояния явными, используя метки:

method ThisFails(t0: T, yes: T, no: T) requires P(yes) && !P(no) {
  var arr := new T[2](_ => t0);
  label initial:
    arr[0] := yes;
  label intermediate:
    arr[1] := no;
  label final:
    assert true;
  assert exists k :: 0 <= k < arr.Length && P(arr[k]); // FAILS
}

Затем достаточно добавить утверждение assert old@intermediate(arr[0]) == old@final(arr[0]);, чтобы подтвердить, что эта часть массива не была изменена.

Другой способ увидеть проблему — воспроизвести проблему с последовательностями:

method ThisFails(t0: T, yes: T, no: T) requires P(yes) && !P(no) {
  var sq := [t0, t0];
  var sq0 := sq[0 := yes];
  var sq1 := sq0[1 := no];
  // We know sq0[0] == yes, but not sq1[0] == yes
  // assert sq1[0] == yes; // Adding this fixes the issue
  assert exists k :: 0 <= k < |sq1| && P(sq1[k]); // FAILS
}

Отличный ответ, спасибо, что показали, как это работает!

James Wilcox 29.11.2022 22:36

Большое спасибо! Я постараюсь пройти через все это :D

arn 30.11.2022 14:02

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