отсутствует инвариант в дафном коде, включающем последовательности

Проблема в том, что ваше определение 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;
  } 
}

Вам также может быть интересно посмотреть этот эпизод Угол проверки на эту тему.

Rustan