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

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-logic это доказано (формально) так (переписав его как цикл 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. Опять же, как в обычной математике.