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