 |
 |
 |
 |
|
 |
 |
126
с, при с
mx
mx
=
= max(a,b,c).
mx, при с < mx
Что и требовалось доказать.
Доказательство лемм
- основной прием доказательства правильности сложных алгоритмов и
программ. Напомним, что лемма — это вспомогательное утверждение, предполагающее отдельное
доказательство.
Одним из важнейших применений аппарата лемм является анализ результатов выполнения и
доказательство правильности алгоритмов с циклами. Используемые для анализа циклов леммы
называются индуктивными утверждениями. Эти леммы выражают утверждения о промежуточных
результатах выполнения циклов.
В качестве примера использования индуктивных рассуждений рассмотрим алгоритм вычисления
среднего арифметического последовательности чисел. В приводимом алгоритме предполагается, что
последовательность чисел размещена в массиве X[1:N].
алг «среднее значение»
массив X[1:N]
нач
Результаты:
от k = 1 до N цикл
S := S * (k-l)/k + X[k]/k
S
k
= S
k-1
*(k-l)/k + X[k]/k
кцикл
[k = (1...N)]
Xcp := S
Xcp = S
кон
Этот алгоритм обычно считается ошибочным (?!). «Ошибкой» в этом алгоритме считается
отсутствие присваивания S := 0 перед началом цикла.
Разберем результаты выполнения алгоритма на первых трех шагах:
S1 = S
0
(l - 1)/1 + Х
1
/1 = S
0
0/1 + Х[1]/1 = Х
1
/1;
S2 = S1
(2 - 1)/2 + Х[2]/2 = S1
1/2 + Х[2]/2 = Х
1
/2 + Х[2]/2;
S3 = S2
(3 - 1)/3 + Х[3]/3 = S2
2/3 + Х[3]/3 = Х[1]/3 + Х[2]/3 + Х[3]/3.
Можно утверждать, что на первых трех шагах результатом является среднее арифметическое
обрабатываемых чисел. На основе этих примеров можно сделать индуктивное утверждение
- «на
каждом очередном k-м шаге выполнения цикла результатом будет среднее арифметическое»
S
k
= S
k-1
(k-l)/k + X[k]/k = X[l]/k + X[2]/k + ... + X[k]/k.
Доказательство этого утверждения проводится с помощью математической индукции. На первом
шаге при k = 1 оно уже доказано. Допустим, что оно справедливо на (k -1)-м шаге
S
k-1
= X[l]/(k-l) + X[2]/(k-l) + ... + X[k-l]/(k-l).
Подставим его в описание результатов цикла на k-м шаге
S
k
= S
k-1
(k-l)/k +X[k]/k.
Тогда результат выполнения цикла на k-м шаге оказывается равным
S
k
= X[l]/k + X[2]/k + ... + X
k-l
/k + X[k]/k,
т. е. среднему арифметическому первых k чисел.