в операторе для последовательностей, соответствующих странным в Дафни

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

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


seq dafny
person Andrici Cezar    schedule 12.05.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Это связано с триггерами квантификатора. Подробнее о триггерах можно прочитать в разделе Часто задаваемые вопросы по Dafny.

В этом случае причина, по которой окончательное утверждение в вашем первом примере не удается, заключается в том, что квантификатор 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} для первого утверждения в первом примере.

person James Wilcox    schedule 12.05.2019