в операторе для странных компиляций последовательностей в Дафни - PullRequest
Новая
       29

в операторе для странных компиляций последовательностей в Дафни

1 голос
/ 12 мая 2019

Как я могу помочь Дафни доказать, что следующие два утверждения одинаковы: 

method foo(xs : seq<int>)
  requires forall x :: x in xs ==> 0 <= x < 5;
{
  assert forall x :: x in xs ==> 0 <= x < 5;
  assert forall i :: 0 <= i < |xs| ==> 0 <= xs[i] < 5;
}

Кроме того, Дафни, похоже, может доказать, что следующие одинаковые.Почему это так? 


predicate test(value : int) {
  0 <= value < 5
}

method foo'(xs : seq<int>)
  requires forall x :: x in xs ==> test(x);
{
  assert forall i :: 0 <= i < |xs| ==> test(xs[i]);
}

Пример на Rise4Fun

1 Ответ

1 голос
/ 13 мая 2019

Это связано с триггерами квантификатора.Подробнее о триггерах можно прочитать в 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} для первого утверждения в первом примере.
...