Тривиальное нарушение утверждения в Дафни

Question

Почему Дафни утверждает, что это простое утверждение возможно нарушено?

var b := new int[2];
b[0],b[1] := 1, -2;
assert exists k | 0 <= k < b.Length :: (b[k] == 1 || b[k] == -1);

Answer 1

Это связано с тем, как Дафни обрабатывает экзистенциальные квантификаторы. Это (почти) никогда не "угадать" значение для вас. Вместо этого Dafny использует синтаксическую эвристику (называемую "триггерами"), чтобы опробовать определенные значения из контекста.

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

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

assert b[0] == 1;

или даже

assert b[0] == 1 || b[0] == -1

---

Это несколько связано с этим вопросом.

Подробнее о триггерах смотрите в этом ответе.