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

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; 
    } 
} 

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

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

Благодарности

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

Answer 1

Что-то вроде этого, может быть, хотя это немного педантичный.

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

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

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

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