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

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

1 голос
/ 24 февраля 2012

Я написал свою собственную тривиальную маленькую функцию (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;
  }
}

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

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

Спасибо

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

1 Ответ

1 голос
/ 27 февраля 2012

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

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

Доказательство: доказательство по индукции.В базовом случае 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;
  }
}

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

Доказательство: доказательство проводится по индукции.В базовом случае 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 (в верхней части цикла).

...