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

Ответ 1

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

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

                  t22 > .

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

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

• Базовый регистр: инвариант цикла сохраняется после записи цикла (после 0 итераций)

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

• Гипотеза индукции. Предположим, что инвариант выполняется в верхней части цикла.

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

  После того, как тело выполнено, 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 < i} 1, если a[x] |k, 0 в противном случае.

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

Ответ 2

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

В случае 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.

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