Почему Дафни утверждает, что это простое утверждение может быть нарушено?
var b := new int[2];
b[0],b[1] := 1, -2;
assert exists k | 0 <= k < b.Length :: (b[k] == 1 || b[k] == -1);
Тривиальное нарушение утверждения в Dafny
Ответы (1)
Это связано с тем, как Дафни обращается с кванторами существования. Он (почти) никогда не «угадает» значение за вас. Вместо этого Дафни использует синтаксическую эвристику (называемую «триггерами»), чтобы пробовать определенные значения из контекста.
В вашем утверждении триггером является b[k], что означает, что Дафни будет пробовать только значения k, в которых явно упоминается выражение b[k].
Таким образом, один из способов исправить утверждение — явно указать правильное значение для k, добавив утверждение
assert b[0] == 1;
или даже
assert b[0] == 1 || b[0] == -1
Это несколько связано с этим вопросом.
Дополнительные сведения о триггерах см. в этом ответе.
person
James Wilcox
schedule
15.05.2018
