Модель Z3 для правильного метода Дафни

То, что говорит Мальте, верно (и я также нашел, что это хорошо объяснено).

Dafny надежен в том смысле, что проверяет только правильные программы. Другими словами, если программа неверна, верификатор Dafny никогда не скажет, что она верна. Однако лежащие в основе проблемы принятия решений, как правило, неразрешимы. Поэтому неизбежно будут случаи, когда программа соответствует своим спецификациям, а верификатор все равно выдает сообщение об ошибке. Действительно, в таких случаях верификатор может даже показать предполагаемый контрпример. Это может быть ложный контрпример (как в приведенном выше примере) — это просто означает, что, насколько может сказать верификатор, это контрпример. Если проверяющий просто потратил немного больше времени или был достаточно умен, чтобы развернуть больше определений функций, применить индукционные гипотезы или сделать множество других хороших вещей, можно определить, что контрпример является поддельным. . Таким образом, любое полученное вами сообщение об ошибке (включая любой контрпример, который может сопровождать такое сообщение об ошибке) следует интерпретировать как возможную ошибку (и возможный контрпример).

Подобные ситуации часто возникают, если вы пытаетесь проверить правильность цикла и не предоставляете достаточно сильный инвариант цикла. Затем верификатор Dafny может показать некоторые значения переменных при входе в цикл, которые никогда не могут возникнуть в действительности. Затем контрпример пытается дать вам представление о том, как соответствующим образом усилить ваш инвариант цикла.

Наконец, позвольте мне добавить два замечания к тому, что сказал Мальте.

Во-первых, в этом примере есть по крайней мере еще один источник неполноты, а именно нелинейная арифметика. Иногда бывает сложно ориентироваться.

Во-вторых, трюк с использованием функции Dummy можно упростить. Достаточно (хотя бы в этом примере) упомянуть вызов Pow, например так:

lemma EvenPowerLemma(a: int, b: nat)
  requires Even(b)
  ensures Pow(a, b) == Pow(a*a, b/2)
{
  if b != 0 {
    var dummy := Pow(a, b - 2);
  }
}

Тем не менее, мне больше нравятся два других ручных доказательства, потому что они лучше объясняют пользователю, что такое доказательство.

Рустан

Дафни не может доказать лемму из-за комбинации двух возможных источников неполноты: рекурсивных определений (здесь Pow) и индукции. Доказательство фактически терпит неудачу из-за слишком малого количества информации, то есть из-за того, что проблема недостаточно ограничена, что, в свою очередь, объясняет, почему можно найти контрпример.

Введение

Автоматизировать индукцию сложно, поскольку для этого требуется вычисление гипотезы индукции, что не всегда возможно. Однако у Дафни есть некоторые эвристики для применения индукции (которые могут работать или не работать), которые можно отключить, как в следующем коде:

lemma {:induction false} EvenPowerLemma_manual(a: int, b: nat)
  requires Even(b);
  ensures Pow(a, b) == Pow(a*a, b/2);
{
  if (b != 0) {
    EvenPowerLemma_manual(a, b - 2);
  }
}

При выключенной эвристике нужно вручную "вызвать" лемму, т.е. использовать предположение индукции (здесь только в случае, когда b >= 2), чтобы провести доказательство.

В вашем случае эвристики были активированы, но они не были «достаточно хороши», чтобы провести доказательство. Я объясню, почему дальше.

Рекурсивные определения

Статические рассуждения о рекурсивных определениях путем их развертывания склонны к бесконечному спуску, потому что в общем случае невозможно решить, когда остановиться. Следовательно, Dafny по умолчанию развертывает определения функций только один раз. В вашем примере развертывания определения Pow только один раз недостаточно, чтобы заставить работать эвристику индукции, потому что гипотеза индукции должна быть применена к Pow(a, b-2), что не «появляется» в доказательстве (поскольку развертывание только один раз приводит вас к Pow(a, b - 1)) . Однако явное упоминание Pow(a, b-2) в доказательстве, даже в бессмысленной формуле, запускает эвристику индукции:

function Dummy(a: int): bool
{ true }

lemma EvenPowerLemma(a: int, b: nat)
  requires Even(b);
  ensures Pow(a, b) == Pow(a*a, b/2);
{
  if (b != 0) {
    assert Dummy(Pow(a, b - 2));
  }
}

Функция Dummy предназначена для того, чтобы убедиться, что утверждение не предоставляет никакой информации, кроме синтаксического включения Pow(a, b-2). Менее странным было бы утверждение assert Pow(a, b) == a * a * Pow(a, b - 2).

Расчетное доказательство

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

lemma {:induction false} EvenPowerLemma_manual(a: int, b: nat)
  requires Even(b);
  ensures Pow(a, b) == Pow(a*a, b/2);
{
  if (b != 0) {
    calc {
         Pow(a, b);
      == a * Pow(a, b - 1);
      == a * a * Pow(a, b - 2);
      == {EvenPowerLemma_manual(a, b - 2);}
         a * a * Pow(a*a, (b-2)/2);
      == Pow(a*a, (b-2)/2 + 1);
      == Pow(a*a, b/2);
    }
  }
}