Элементы доказательного программирования - часть 8
Sk
= Sk-1×(k-l)/k + X[k]/k = X[l]/k + X[2]/k + ... + X[k]/k.
Доказательство этого утверждения проводится с помощью математической индукции. На первом шаге при k = 1 оно уже доказано. Допустим, что оно справедливо на (k -1)-м шаге
Sk-1
= X[l]/(k-l) + X[2]/(k-l) + ... + X[k-l]/(k-l).
Подставим его в описание результатов цикла на k-м шаге
Sk= Sk-1×(k-l)/k +X[k]/k.
Тогда результат выполнения цикла на k-м шаге оказывается равным
Sk
= X[l]/k + X[2]/k + ... + X[k-l]/k + X[k]/k,
т. е. среднему арифметическому первых k чисел.
Таким образом, индуктивное утверждение доказано. В силу математической индукции это утверждение верно для всех k = l, 2, ..., N. Следовательно, на последнем шаге конечным результатом выполнения цикла станет значение
SN
= SN-1×(N-1) + X[N]/N = X[1]/N + ... + X[N]/N.
Исходя из этого утверждения конечным результатом выполнения алгоритма в целом будет среднее арифметическое значение
Xcp = SN = X[1]/N + ... + X[N]/N.
Следовательно, приведенный алгоритм, несмотря на содержащуюся в нем «ошибку», является правильным. В целом анализ правильности алгоритмов с циклами во многом построен на использовании индукции.
Индукция - это вывод общих суждений из частных примеров. При анализе циклов она используется для подбора индуктивных утверждений о промежуточных результатах выполнения циклов. Однако для доказательства правильности индуктивных утверждений о результатах выполнения циклов используется полная математическая индукция.
Математическая индукция - это принцип доказательства последовательностей утверждений Р(1), Р(2), Р(3), ..., P(N), .... когда известно, что верны первые утверждения для n = 1, 2, 3 и из истинности (n - 1)-го утверждения следует истинность n-го утверждения:
Принцип математической индукции:
если первое утверждение Р(1) истинно
и из утверждения Р(n - 1) следует
утверждение Р(n), то истинны все
утверждения Р(1), Р(2), Р(3), ..., Р(n), ... .
Приведем примеры индуктивного анализа циклов для алгоритма нахождения минимального значения в последовательности чисел, который в этот раз действительно будет ошибочным.