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 не помогает.
Что означает эта ошибка? Как я могу убедить Дафни, что это нормально?
Сообщение об ошибке указывает на то, что Дафни не может доказать, что значение, присвоенное q, действительно является nat, как того требует тип q. Это странно, потому что ваши делимое и делитель неотрицательны. Верификатор, как правило, неплохо справляется с линейной арифметикой, но ваш пример выходит за рамки линейной арифметики (поскольку делитель не является буквальной константой), и тогда верификатор более ненадежен.
Поигравшись с этим, я предполагаю, что вычитание в знаменателе каким-то образом предварительно обрабатывается, что затрудняет для верификатора применение того, что он знает о нелинейном делении. Мне удалось найти обходной путь, дав термину d - 1 имя, например:
method Div(n: nat, d: nat) returns (q: nat)
requires d > 1
{
var y := d - 1;
q := n / y;
}
Рустан
Я думаю, проблема в том, что тип (d - 1) равен int.
Это исправляет это:
let d1: nat = d - 1;
q := n / d1;
Мое намерение с этим кодом заключалось в том, что все операции должны быть nat арифметическими. У Дафни были другие идеи. Вот что, по моему мнению, происходит (дальше предположения):
У Дафни есть начальный этап определения типа, который происходит перед запуском доказывающего устройства. Этот алгоритм не может использовать утверждения и предварительные условия; он только проверяет их тип. Он не «знает», что d - 1 гарантированно будет положительным, или даже что d > 1.
Таким образом, для проверки типов Дафни, когда d является nat, d - 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);
}
Разумеется, Dafny 2.1.1.10209 не может доказать постусловие.
nat на nat как int. Итак, причина, по которой ваше исправление работает, заключается в том, что вы вводите новую переменную.
- person Rustan Leino; 18.05.2018
a / b и a % b дают натуральное число, если a и b — натуральные числа (а b не равно нулю).
- person Rustan Leino; 22.05.2018
d - 1 было достаточно, поэтому я остановился на этом. Возможно, что верификатор выполняет другую перезапись для вычитания, чем для сложения. Жаль, что не могу поставить более точный диагноз.
- person Rustan Leino; 22.05.2018
