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

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

0 голосов
/ 19 января 2019

Мне интересно, есть ли причина, по которой dafny не может проверить мою программу?

https://rise4fun.com/Dafny/Ip1s

Мне не хватает какого-то дополнительного инварианта?

1 Ответ

0 голосов
/ 21 января 2019

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

...