Доказательство введением псевдокода

Question

Я не очень понимаю, как использовать доказательство по индукции на psuedocode. Кажется, это не работает так же, как использование его в математических уравнениях.

Я пытаюсь подсчитать количество целых чисел, которые делятся на k в массиве.

Algorithm: divisibleByK (a, k)
Input: array a of n size, number to be divisible by k
Output: number of numbers divisible by k

int count = 0;
for i <- 0 to n do
    if (check(a[i],k) = true)
        count = count + 1
return count;


Algorithm: Check (a[i], k)
Input: specific number in array a,  number to be divisible by k
Output: boolean of true or false

if(a[i] % k == 0) then
    return true;
else    
    return false;

Как можно доказать, что это правильно? Спасибо

Answer 1

В этом случае я бы интерпретировал "индуктивно" как "индукцию по количеству итераций".

Для этого мы сначала устанавливаем так называемый инвариант петли. В этом случае инвариант цикла:

count хранит количество чисел, делимых на k с индексом ниже чем i ,

Этот инвариант сохраняется при входе в цикл и гарантирует, что после цикла (когда i = n) count содержит количество значений, делимых на k во всем массиве.

Индукция выглядит так:

1. Базовый случай: инвариант цикла сохраняется при входе в цикл (после 0 итераций)

   поскольку i равно 0, элементы не имеют индекс ниже i, Поэтому нет элементов с индексом меньше i делятся на k, Таким образом, так как count равно 0, инвариант имеет место.

2. Индукционная гипотеза: мы предполагаем, что инвариант выполняется в верхней части цикла.

3. Индуктивный шаг. Покажем, что инвариант имеет место в нижней части тела цикла.

   После того, как тело было выполнено, i был увеличен на единицу. Для инварианта цикла, чтобы держать в конце цикла, count должны быть скорректированы соответственно.

   Так как теперь есть еще один элемент (a[i]) который имеет индекс меньше чем (новый) i, count должен был быть увеличен на единицу, если (и только если) a[i] делится на k, что именно то, что обеспечивает if-утверждение.

   Таким образом, инвариант цикла сохраняется и после того, как тело было выполнено.

QED.

---

В Hoare-логике это доказано (формально) примерно так (переписав это как цикл while для ясности):

{ I }
{ I[0 / i] }
i = 0
{ I }
while (i < n)
    { I ∧ i < n }
    if (check(a[i], k) = true)
        { I[i + 1 / i] ∧ check(a[i], k) = true }
        { I[i + 1 / i][count + 1 / count] }
        count = count + 1
        { I[i + 1 / i] }
    { I[i + 1 / i] }
    i = i + 1
    { I }
{ I ∧ i ≮ n }
{ count = ∑ 0 x < n;  1 if a[x] ∣ k, 0 otherwise. }

куда I (инвариант) это:

count = ∑ _{x 1, если a[x] ∣ k, 0 в противном случае.}

(Для любых двух последовательных строк утверждения ({...}) есть обязательство доказательства (первое утверждение должно подразумевать следующее), которое я оставляю как упражнение для читателя;-)

Answer 2

Мы доказываем правильность по индукции на nколичество элементов в массиве. Ваш диапазон неверен, он должен быть от 0 до n-1 или от 1 до n, но не от 0 до n. Мы примем 1 к п.

В случае n=0 (базовый случай) мы просто проходим алгоритм вручную. counter инициируется со значением 0, цикл не повторяется, и мы возвращаем значение счетчика, которое, как мы сказали, было 0. Это правильно.

Мы можем сделать второй базовый случай (хотя это и не нужно, как в обычной математике). п =1. Счетчик инициализируется с 0. Цикл делает один проход, в котором i принимает значение 1, и мы увеличиваем counter если первое значение в a делится на k (что верно из-за очевидной правильности Check алгоритм).
Поэтому мы возвращаем 0, если a[1] не делится на k, а в противном случае мы возвращаем 1. Этот случай также работает.

Индукция проста. Мы предполагаем корректность для n-1 и докажем для n (опять же, как в обычной математике). Чтобы быть должным образом формальным, отметим, что counter содержит правильное значение, которое мы возвращаем к концу последней итерации в цикле.

По нашему предположению мы знаем, что после n-1 итераций counter содержит правильное значение относительно первых n-1 значений в массиве. Мы вызываем базовый случай n=1, чтобы доказать, что он добавит 1 к этому значению, если последний элемент делится на k, и, следовательно, конечное значение будет правильным значением для n.

QED.

Вам просто нужно знать, на какую переменную производить индукцию. Обычно размер ввода наиболее полезен. Кроме того, иногда вам нужно предполагать правильность для всех натуральных чисел меньше, чем n, иногда просто n-1. Опять же, как и в обычной математике.