Информатика


Элементы доказательного программирования - часть 7


Доказательство. В силу предположения предшествующее значе­ние переменной mx = max(a,b). Отсюда получаем, что

 с, при с ³ 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                       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-м шаге выполнения цикла результатом будет среднее арифметическое»




Начало  Назад  Вперед