Мне интересно, есть ли причина, по которой Дафни не может проверить мою программу?
https://rise4fun.com/Dafny/Ip1s
Я пропустил какой-то дополнительный инвариант?
Проблема в том, что ваше определение s
и ваша конструкция o
идут в «разных направлениях». Рекурсивный случай s
определяет s(i)
с точки зрения
i[0]
и то, что «ранее» определено s(i[1..])
. Напротив, итерация цикла определяет новый o
с точки зрения i[n]
и предыдущего значения o
. Потребуется индуктивно доказанная лемма, чтобы установить обязательства доказательства в вашей текущей программе, и Дафни не изобретает такие леммы сам по себе.
Для записи в этом ответе вот с чего вы начали:
function s(i: seq<int>): seq<int> {
if |i| == 0 then [] else
if i[0] == 42 then [i[0]] + s(i[1..])
else s(i[1..])
}
method q (i: seq<int>) returns (o: seq<int>)
ensures o == s(i)
{
var n := 0;
o := [];
while n < |i|
invariant n <= |i| && o == s(i[..n])
{
if i[n] == 42 {
o := o + [i[n]];
}
n := n + 1;
}
}
Есть четыре выхода.
Один из выходов — определить другую версию s
, назовем ее s'
, которая рекурсирует с другого конца заданной последовательности. Затем замените s
на s'
в спецификации метода и инварианте цикла. Это прекрасное решение, если по какой-то причине вы действительно не предпочитаете s
, а не s'
, в спецификации вашего метода.
Второй выход — определить такой s'
и доказать лемму, что s(i)
и s'(i)
возвращают одно и то же значение. Это позволит вам сохранить s
в спецификации метода за счет наличия двух определений функций и необходимости писать (и доказывать и использовать) лемму.
Третий выход — изменить цикл так, чтобы он выполнялся «вниз», а не «вверх». То есть запустите n
с |i|
и уменьшите значение n
в теле цикла. (Как обычно, приращение n
обычно лучше всего выполнять в конце тела цикла (пост-инкремент), тогда как уменьшение n
обычно лучше всего выполнять в начале тела цикла (до декремента).)
Четвертый выход — изменить способ написания инварианта цикла для o
. В настоящее время инвариант говорит о том, что вы уже вычислили, то есть o == s(i[..n])
. Вместо этого вы можете написать инвариант с точки зрения того, что еще предстоит вычислить, как в o + s(i[n..]) == s(i)
, который вы можете прочитать как «как только я добавлю s(i[n..])
к o
, у меня будет s(i)
». Вот эта версия q
:
method q(i: seq<int>) returns (o: seq<int>)
ensures o == s(i)
{
var n := 0;
o := [];
while n < |i|
invariant n <= |i| && o + s(i[n..]) == s(i)
{
if i[n] == 42 {
o := o + [i[n]];
}
n := n + 1;
}
}
Вам также может быть интересно посмотреть этот выпуск Verification Corner на эту тему.
Рустан