Это связано с триггерами квантификатора.Подробнее о триггерах можно прочитать в Dafny FAQ .
. В этом случае причина, по которой окончательное утверждение не выполняется в первом примере, состоит в том, что квантификатор forall
в предложении requires
и первое утверждение срабатывает x in xs
. 1 . Это означает, что этот количественный факт не будет использоваться при значении v
, за исключением случаев, когда v in xs
находится "в области действия" дляверификатор.Чтобы доказать второе утверждение, верификатор должен использовать ранее определенный количественно факт со значением xs[i]
, но xs[i] in xs
не находится "в области видимости".Это может звучать странно, потому что xs[i] in xs
всегда верно, но оказывается, что верификатор не может выяснить это без вашей помощи.
Итак, чтобы доказать второе утверждение, вам нужно получить факт xs[i] in xs
по объему как-то.Один из способов - изменить утверждение на
assert forall i :: 0 <= i < |xs| ==> xs[i] in xs && 0 <= xs[i] < 5;
(добавив xs[i] in xs
к заключению).Фактически, как только это новое утверждение доказано, Дафни может , а затем доказать ваше второе утверждение впоследствии, потому что это новое утверждение срабатывает на xs[i]
, что также «в рамках» в вашем втором утверждении.
Наконец, причина вашего второго примера в том, что введение предиката test
изменило доступные триггеры.Теперь forall
из условия requires
запускается как для x in xs
, так и для test(x)
.Новый триггер совпадает в новой версии утверждения в теле foo
, так как test(xs[i])
уже появляется.Это приводит к тому, что первый forall
создается правильно, что означает, что утверждение проходит.Подобные бесполезные именованные предикаты, подобные этому, являются обычной уловкой, когда вы массируете триггеры, чтобы заставить их делать то, что вы хотите.
1. Чтобы увидеть, какие триггеры используются, наведите указатель мыши на
forall
в вашей IDE или запустив в командной строке с опцией
/printTooltips
.Вы должны увидеть что-то вроде
Selected triggers: {x in xs}
для первого утверждения в первом примере.