Может ли Дафни проверить суммирование элементов справа?

Теперь давайте переместим утверждение еще на одну строку вверх по присваиванию r := r + input[i];. Опять же, хитрость заключается в том, чтобы вручную отменить это назначение, заменив r на r + input[i] в утверждении, например:

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    assert r + input[i] == sumSpecR(input[..i+1]);  // moved this assertion up one line
    r := r + input[i];
    i := i + 1;
  }

Опять же, Дафни сообщает о нарушении утверждения, но не о нарушении инварианта. (И, опять же, если бы мы ошиблись, он бы сообщил о нарушении инварианта.)

Теперь у нас есть утверждение в верхней части цикла, где мы знаем, что инвариант выполняется. Пришло время сделать доказательство.

Мы пытаемся доказать уравнение. Мне нравится использовать оператор Дафни calc для отладки доказательств уравнений. Если вы не знакомы с оператором calc, основная форма

calc {
  A;
  B;
  C;
  D;
}

что доказывает A == D, доказывая A == B, B == C и C == D. Это дает удобный способ добавить промежуточные шаги к эквациональному доказательству и точно определить, где Дафни запутался.

Чтобы преобразовать утверждение уравнения в утверждение calc, мы можем просто поместить левую часть уравнения в первую строку, а правую часть во вторую строку. Пока это ничего не меняет, но давайте просто убедимся:

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    // replaced old assertion with the following calc statement
    calc {
      r + input[i];
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

Дафни сообщает об ошибке в операторе calc, но не в операторе invariant, так что мы по-прежнему знаем, что доказываем правильный факт, чтобы завершить проверку цикла.

Ошибка находится во второй строке тела оператора calc, и в сообщении говорится, что шаг вычисления между предыдущей строкой и этой строкой может не выполняться. По сути, Дафни не смог доказать, что две линии равны. Неудивительно, поскольку мы создали этот оператор calc из ошибочного утверждения.

Теперь мы можем начать добавлять промежуточные шаги. Иногда имеет смысл двигаться вперед от верхней строки, а в других случаях имеет смысл работать от последней строки вверх. Я думаю, что вторая стратегия имеет больше смысла здесь.

Давайте вручную развернем определение sumSpecR и посмотрим, где мы застряли. Глядя на определение sumSpecR, он сначала проверяет, является ли |input| == 0. Будьте осторожны, потому что input здесь относится к аргументу sumSpecR, не к аргументу sumRightChange! В контексте последней строки нашего оператора calc мы передаем input[..i+1] в sumSpecR, поэтому определение спрашивает, имеет ли этот список нулевую длину. Но мы знаем, что это не так, так как i >= 0 и мы добавляем к нему 1. Итак, мы окажемся в else ветке определения.

Ветвь else разделяет список справа. Давайте попробуем быть систематичными и просто скопируем-вставим ветку else определения, заменив фактический аргумент input[..i+1] на имя параметра input. (Мне нравится использовать текстовый редактор для поиска и замены на этом шаге.)

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      // added the following line by copy-pasting the else branch of the 
      // definition of sumSpecR and then replacing its parameter
      // input with the actual argument input[..i+1]
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

Теперь обратите внимание на то, что происходит с сообщением об ошибке. Он движется вверх по строке! Это означает, что мы делаем успехи, потому что Дафни согласен с нами в том, что наша новая средняя строка тела оператора calc равна последней строке.

Сейчас мы можем сделать множество упрощений. Начнем с упрощения |input[..i+1]| до i+1. Вы можете сделать это, изменив строку, которую мы только что добавили, но мне нравится делать это, добавляя еще одну строку над ней, чтобы я мог записывать свой прогресс и убедиться, что Дафни согласен с тем, что я двигаюсь в правильном направлении.

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      // added the following line simplifying |input[..i+1]| into i+1
      input[..i+1][i+1-1] + sumSpecR(input[..i+1][..i+1-1]);
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

Опять же, сообщение об ошибке перемещается вверх по строке. Ура!

Теперь мы можем упростить i+1-1 до i, а также input[..i+1][i] до input[i]. Опять же, я предпочитаю делать это на новой строке.

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      input[i] + sumSpecR(input[..i+1][..i]);  // added this line
      input[..i+1][i+1-1] + sumSpecR(input[..i+1][..i+1-1]);
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

Сообщение об ошибке продолжает двигаться вверх.

Следующее упрощение, которое я хотел бы сделать, это преобразовать input[..i+1][..i] в input[..i]. Опять же, я использую новую строку.

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      input[i] + sumSpecR(input[..i]);  // added this line
      input[i] + sumSpecR(input[..i+1][..i]);
      input[..i+1][i+1-1] + sumSpecR(input[..i+1][..i+1-1]);
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

Внимательно следите за тем, что происходит с сообщением об ошибке. Он не двигается! Это говорит нам о двух вещах. Во-первых, Дафни не согласен с нашим последним упрощением. Во-вторых, Дафни говорит, что наша новая добавленная строка равна первой строке оператора calc! (Здесь Дафни использует предположение об инварианте цикла, сообщающем нам r == sumSpecR(input[..i]).) Таким образом, хотя мы работали с последней строки вверх, теперь мы фактически достигли вершины с оставшимся пробелом между строками 2 и 3.

Значит, Дафни этого не видит.

input[i] + sumSpecR(input[..i]) == input[i] + sumSpecR(input[..i+1][..i])

Что дает? Выражение input[i] появляется с обеих сторон, поэтому остается показать следующее:

sumSpecR(input[..i]) == sumSpecR(input[..i+1][..i])

Здесь у нас есть функция sumSpecR, примененная к двум синтаксически различным аргументам, которые, как мы считаем, одинаковы. На данный момент не имеет значения, каково определение sumSpecR, важно только то, что это функция, применяемая к равным аргументам. Таким образом, мы можем попытаться проверить, что аргументы действительно равны.

assert input[..i] == input[..i+1][..i];

И это утверждение нам было нужно, чтобы получить полное доказательство.

В конце такого процесса отладки я обычно подчищаю и оставляю только те факты, которые действительно нужны Дафни для доказательства. Поэтому я просто пытаюсь удалить материал и посмотреть, работает ли доказательство. В этом случае требуется только самое последнее обнаруженное нами утверждение; все остальное можно удалить.

Вот мой последний цикл:

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    assert input[..i] == input[..i+1][..i];  // load-bearing assertion due to sequence extensionality
    r := r + input[i];
    i := i + 1;
  }

Мне нравится оставлять себе маленькую заметку, напоминающую мне, что я думаю, что доказательство не будет работать без этого утверждения, вместе с моими лучшими предположениями о том, почему это утверждение необходимо.