В Dafny, как я могу исправить ошибку «значение не удовлетворяет ограничениям подмножества nat» при делении?

Question

Это Дафни код :

method Div(n: nat, d: nat) returns (q: nat)
  requires d > 1
{
  q := n / (d - 1);
}

выдает эту ошибку:

Dafny 2.1.1.10209
stdin.dfy(4,9): Error: value does not satisfy the subset constraints of 'nat'

Dafny program verifier finished with 0 verified, 1 error

Строка 4, столбец 9 - символ /, обозначающий деление.

Утверждение, что d - 1 != 0 не помогает.

Что означает эта ошибка? Как я могу убедить Дафни, что это нормально?

Answer 1

Сообщение об ошибке указывает, что Дафни не может доказать, что значение, присвоенное q, действительно является nat, как того требует тип q. Это странно, потому что ваш дивиденд и делитель неотрицательны Верификатор, как правило, достаточно хорош в линейной арифметике, но ваш пример выходит за рамки линейной арифметики (поскольку делитель не является литеральной константой), и тогда верификатор более ненадежен.

Играя с этим, я предполагаю, что вычитание в знаменателе подвергается какой-то предварительной обработке, что затрудняет для верификатора применять то, что он знает о нелинейном делении. Я смог найти обходной путь, дав термину d - 1 имя, например:

method Div(n: nat, d: nat) returns (q: nat)
  requires d > 1
{
  var y := d - 1;
  q := n / y;
}

Rustan

Answer 2

Я думаю, что проблема в том, что тип (d - 1) равен int.

Это исправляет это:

let d1: nat = d - 1;
q := n / d1;

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

• У Дафни есть начальный проход вывода типа, который происходит за до того, как запускается проверяющим.Этот алгоритм не имеет возможности использовать утверждения и предварительные условия;это только проверяет их тип.Он не «знает», что d - 1 гарантированно будет положительным или даже что d > 1.

• То есть для проверки типа Дафни, когда d является natd - 1 должно быть int.Результат вычитания nat из nat может быть отрицательным.

• Учитывая это, не очевидно, что эта программа хорошо напечатана.Но это нормально!Вывод типа Дафни может просто отложить суждение по этому вопросу.Это позволяет использовать n / (d - 1) в качестве nat здесь, и делает отметку, чтобы проверить, что значение n / (d - 1) действительно гарантированно попадет в подмножество nat его типа int.

• Удивительно, но проверяющий не может справиться с этим.Я проверил, изменив тип возврата так, чтобы проверка типов прошла без заминки:

  method Div(n: nat, d: nat) returns (q: int)
    requires d > 1
    ensures q >= 0
  {
    q := n / (d - 1);
  }
  

  Конечно, Дафни 2.1.1.10209 не может доказать постусловие.