Дафни: Какие термины не найдены, чтобы вызвать на среднее значение?

Question

В Дафни я получаю предупреждение о том, что мои квантификаторы

No terms found to trigger on.

Что я пытаюсь сделать для своего кода, так это найти наибольшее число, имеющее квадратное значение, которое меньше или равно заданному натуральному числу "n". Вот код, который я придумал до сих пор:

method sqrt(n : nat) returns (r: int)
  // square less than or equal to n
  ensures (r * r) <= n 
  // largest number
  ensures forall i :: 0 <= i < r ==> (i * i) < (r * r)
{
    var i := 0; // increasing number
    r := 0;
    while ((i*i) <= n)
      invariant (r*r) <= n
      invariant forall k :: 0 <= k < r ==> (k*k) < (r*r)
      decreases n - i
    {
      r := i;
      i := i + 1;
    }

    return r;
}

В этом фрагменте я проверяю, что я возвращаю значение, имеющее квадратное значение, которое меньше или равно n, используя постусловие ensures (r * r) <= n,

Я также пытаюсь проверить, что возвращаемое значение действительно является наибольшим значением, которое имеет квадратное значение, которое меньше или равно 'n', используя квантификатор forall i :: 0 <= i < r ==> (i*i) < (r*r)

Этот квантификатор означает, что все элементы, которые были до 'r', имеют квадратное значение, которое меньше квадратного значения r.

Как можно исправить No terms found to trigger on.? Что это на самом деле означает?

Дафни говорит мне, что это предупреждение. Значит ли это, что мои кванторы неверны? или это означает, что Дафни вообще не может это проверить, но это правильно?

Answer 1

Предупреждение связано с тем, как Dafny (и базовый решатель Z3) обрабатывают квантификаторы.

Прежде всего, это действительно предупреждение. Если в программе нет ошибок (как в вашем примере), то она прошла верификатор и удовлетворяет своей спецификации. Вам не нужно исправлять предупреждение.

Однако в более сложных программах вы часто обнаруживаете, что предупреждение сопровождается неудачными или непредсказуемыми результатами проверки. В этих случаях стоит знать, как это исправить. Часто предупреждение можно устранить, введя бесполезную вспомогательную функцию, которая будет служить триггером.

Например, вот версия вашего примера, где Dafny не предупреждает о триггерах

function square(n: int): int
{
    n * n
}

method sqrt(n : nat) returns (r: int)
  // square less than or equal to n
  ensures r * r <= n
  // largest number
  ensures forall i :: 0 <= i < r ==> square(i) < r * r
{
    var i := 0; // increasing number
    r := 0;
    while i * i <= n
      invariant r * r <= n
      invariant forall k :: 0 <= k < r ==> square(k) < r * r 
      decreases n - i
    {
      r := i;
      i := i + 1;
    }

    return r;
}

Все, что я сделал, это ввел новую функцию square(n) определено быть n * n, а затем использовал его в нескольких ключевых местах под квантификаторами в остальной части программы.

Если все, что вас волнует, это получить этот пример для проверки, вы можете перестать читать здесь. Остальная часть ответа пытается объяснить, почему это исправление работает.

---

Короче говоря, это работает, потому что теперь Дафни может использовать square(i) а также square(k) как триггеры для двух квантификаторов.

Но что такое триггер в любом случае, и почему square(i) действительный триггер, но i * i нет?

Что такое триггер?

Триггер - это синтаксический паттерн, включающий количественные переменные, который служит эвристическим для того, чтобы решатель что-то делал с квантификатором. С forall квантификатор, триггер сообщает Дафни, когда создавать экземпляр квантифицированной формулы с другими выражениями. В противном случае Дафни никогда не будет использовать количественную формулу.

Например, рассмотрим формулу

forall x {:trigger P(x)} :: P(x) && Q(x)

Здесь аннотация {:trigger P(x)} отключает автоматический вывод триггера Дафни и вручную указывает триггер P(x), В противном случае Дафни предположил бы, что P(x) а также Q(x) как триггеры, что обычно лучше, но хуже для объяснения триггеров:).

Этот триггер означает, что всякий раз, когда мы упоминаем выражение вида P(...) квантификатор будет создан, а это означает, что мы получаем копию тела квантификатора с ... подключен для x,

Теперь рассмотрим эту программу

method test()
    requires forall x {:trigger P(x)} :: P(x) && Q(x)
    ensures Q(0)
{
}

Дафни жалуется, что не может проверить постусловие. Но это логически очевидно! Просто вставьте 0 для x в предварительном условии, чтобы получить P(0) && Q(0), что подразумевает постусловие Q(0),

Дафни не может проверить этот метод из-за нашего выбора триггеров. Поскольку постусловие упоминает только Q(0) и ничего о P, но квантификатор срабатывает только P Дафни никогда не будет создавать предварительное условие.

Мы можем исправить этот метод, добавив, казалось бы, бесполезное утверждение

assert P(0);

к телу метода. Весь метод теперь проверяет, включая постусловие. Зачем? Потому что мы упомянули P(0), который вызвал квантификатор из предварительного условия, в результате чего решатель учиться P(0) && Q(0), что позволяет доказать постусловие.

Найдите минутку и поймите, что только что произошло. У нас был логически правильный, но не проверяемый метод, и мы добавили к нему логически неуместное, но верное утверждение, в результате чего верификатор неожиданно преуспел. Другими словами, верификатор Дафни может иногда зависеть от логически нерелевантных влияний, чтобы добиться успеха, особенно когда задействованы квантификаторы.

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

(В дополнение отметим, что этот пример проходит без неуместного утверждения, если мы позволим Дафни выводить триггеры вместо того, чтобы вручную его обрабатывать.)

Что делает хороший триггер?

Хорошими триггерами обычно являются небольшие выражения, содержащие количественные переменные, которые не содержат так называемых "интерпретируемых символов", которые для наших целей можно считать "арифметическими операциями". Арифметика не допускается в триггерах по той причине, что решатель не может легко определить, когда был упомянут триггер. Например, если x + y был разрешенным триггером, и программист упомянул (y + 0) * 1 + xу решателя возникнут проблемы с немедленным признанием того, что это было равно выражению запуска. Так как это может вызвать противоречивую реализацию квантификаторов, арифметика запрещена в триггерах.

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

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