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

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

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

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

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

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

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

assert arr[0] < 0;

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

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

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, но мы не знаем этого по умолчанию во втором (сломанном) сломанном примере.

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

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

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

Если вы наведете курсор на квантификатор, вы увидите 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
}