Буги странно утверждают (ложно) поведение

Question

Я работаю с Буги, и я столкнулся с некоторыми видами поведения, которые я не понимаю.

Я использую assert(false) как способ проверить, если предыдущий assume заявления абсурдны.

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

type T;
const t1, t2: T;
procedure test()
{
  assume (t1 == t2);
  assume (t1 != t2);
  assert(false);
}

...как t1 == t2 && t1 != t2 это абсурдное утверждение.

С другой стороны, если у меня есть что-то вроде

type T;
var map: [T]bool;
const t1, t2: T;

procedure test()
{
  assume(forall a1: T, a2: T :: !map[a1] && map[a2]);
  //assert(!map[t1]);
  assert(false);
}

assert(false) происходит сбой только тогда, когда закомментированная строка не закомментирована. Почему прокомментированное утверждение меняет результат assert(false)?

Answer 1

Суть: SMT-решатель, лежащий в основе Boogie, не будет создавать экземпляр квантификатора, если вы не упомянули наземный экземпляр map[...] в вашей программе.

Вот почему: решатели SMT (которые используют электронное сопоставление) обычно используют синтаксическую эвристику, чтобы решить, когда создавать экземпляр квантификатора. Рассмотрим следующий квантификатор:

forall i: Int :: f(i)

Этот квантификатор допускает бесконечно много экземпляров (так как i распространяется на неограниченную область), попытка всех приведет к не прекращению. Вместо этого решатели SMT ожидают синтаксических подсказок, инструктирующих его, для которых i квантификатор должен быть создан. Эти подсказки называются шаблонами или триггерами. В буги их можно записать так:

forall i: Int :: {f(i)} f(i)

Этот триггер инструктирует решателю SMT создавать квантификатор для каждого i для которого f(i) упоминается в программе (или, скорее, текущий поиск доказательства). Например, если вы предполагаете f(5), тогда квантификатор будет создан с 5 заменил i,

В вашем примере вы не предоставляете шаблон явно, поэтому SMT-решатель может выбрать его для вас, проверив тело квантификатора. Скорее всего подберут {map[a1], map[a2]} (допускается применение нескольких функций, шаблоны должны охватывать все количественные переменные). Если вы раскомментируете предположение, термин "земля" map[t1] становится доступным, и решатель SMT может создать экземпляр квантификатора с a1, a2 сопоставлены с t1, t1, Следовательно, противоречие получено.

См. Руководство Z3 для более подробной информации о шаблонах. Более сложные тексты о шаблонах можно найти, например, в этом документе, в этом документе или в этом документе.