Доказательство корректности с помощью инварианта цикла (индукция)

Question

Я написал свою собственную тривиальную маленькую функцию (php для удобства) и надеялся, что кто-то может помочь структурировать доказательство по индукции для него, просто чтобы я мог получить очень простое представление об этом.

function add_numbers($max) {
  //assume max >= 2
  $index=1;
  $array=array(0);
  while ($index != $max) {
     //invariant: ∀ k:1 .. index-1, array[k]=array[k-1]+1
     $array[$index] = $array[$index-1]+1;
     $index += 1;
  }
}

В результате значение в каждом индексе совпадает с самим индексом, хотя только потому, что a[0] было инициализировано равным 0.

Я полагаю, что цель состоит (или должна быть) в том, чтобы доказать, что инвариант (который сам может быть подозрительным, но, мы надеемся, поможет понять), выполняется для k+1.

Спасибо

редактировать: примеры: http://homepages.ius.edu/rwisman/C455/html/notes/Chapter2/LoopInvariantProof.htm

Answer 1

Может быть, как-то так, хотя это немного педантично.

Инвариант: когда index = n, для n >= 1 (в верхней части цикла, где проверяется условие), массив [i] = i для 0 <= i

Доказательство: доказательство по индукции. В базовом случае n = 1, цикл проверяет условие в первый раз, тело не выполнено, и у нас есть внешняя гарантия, что array[0] = 0, ранее в коде. Предположим, что инвариант выполняется для всех n с точностью до k. Для k + 1 мы присваиваем массив [k] = массив [k-1] + 1. Из предположения индукции массив [k-1] = k-1, поэтому значение, присвоенное массиву [k], равно (k-1)+1 = к. Таким образом, инвариант выполняется для следующего и по индукции каждого значения n (в верхней части цикла).

РЕДАКТИРОВАТЬ:

function add_numbers($max) {
  //assume max >= 2
  $index=1;
  $array=array(63);
  while ($index != $max) {
     //invariant: ∀ k:1 .. index-1, array[k]=array[k-1]+1
     $array[$index] = $array[$index-1]+1;
     $index += 1;
  }
}

Инвариант: когда index = n, для n >= 1 (в верхней части цикла, где проверяется условие), массив [i] = i + 63 для 0 <= i

Доказательство: доказательство по индукции. В базовом случае n = 1, цикл проверяет условие в первый раз, тело не выполнено, и у нас есть внешняя гарантия, что array[0] = 63, ранее в коде. Предположим, что инвариант выполняется для всех n с точностью до k. Для k + 1 мы присваиваем массив [k] = массив [k-1] + 1. Из предположения индукции массив [k-1] = (k-1) + 63 = k + 62, поэтому значение присваивается массиву [k] равно (k+62)+1 = k+63. Таким образом, инвариант выполняется для следующего и по индукции каждого значения n (в верхней части цикла).