 |
 |
 |
 |
|
 |
 |
128
mn
k
= min (x[k], Min(x[k-l], ..., х[1], mn
0
) = Min (x[k], x
k-1], ..., х[1], mn
0
).
В силу математической индукции это утверждение справедливо при k = N:
mn
N
= Min (x[N], x[N - 1], ..., x[2], х[1], mn
0
).
Таким образом на основании этого утверждения можно сделать заключение о конечном результате
выполнения алгоритма в целом:
Min = mn
N
= Min (x[N], x[N - 1], ..., x[2], х[1], mn
0
).
Из этой формулы видно, что конечный результат равно как и результат первого присваивания
зависит от начального значения mn
0
переменной mn. Однако эта величина не имеет определенного
значения, соответственнно неопределен и конечный результат выполнения алгоритма в целом, что и
является ошибкой.
В самом деле, если значение mn
0
окажется меньше любого из значений последовательности х[1], ....
x[N], то конечный результат вычислений будет неправильным. В частности, при реализации алгоритма
на Бейсике неправильный результат будет получен, если последовательность будет состоять только из
положительных чисел. Например, для последовательности чисел: 1, 2, 3, ..., N.
Приведем правильную версию алгоритма с доказательством отсутствия ошибок, используя технику
индуктивных утверждений.
алг «нахождение минимума»
массив х[1:п]
нач
тп := x[1]
от k = 1 до N цикл
если x[k] < тп то
тп = x[k]
все
кцикл
Min = тп
кон
Результаты:
mn
0
= х[1]
[k = (1 ... N)]
случае
ином
в
,
mn
mn
x[k]
при
],
k
[
x
mn
1
-
k
1
-
k
k
Min = mn
N
Утверждение. Для любой последовательности чисел x[l:N] конечным результатом вычислений будет
значение Min = Min (х[1], ..., x[N]).
Доказательство. Воспользуемся результатами анализа выполнения алгоритма, рассмотренного
ранее. Различие между ними состоит в добавлении перед началом цикла присваивания mn := х[1],
которое задает начальное значение переменной mn, равное mn
0
= х[1].
Тогда в силу приведенных ранее рассуждений и выкладок конечным результатом выполнения новой
версии алгоритма будет значение
Min = mn
N
= Min(x[N], x[N-l], ..., х[2], х[1], mn
0
) =
= Min(x[N], x[N-l], ..., x[2
, x[l], x[l]) = Min(x[N], .... х[1]).
Что и требовалось.
Рассмотренные примеры являются образцами доказательств правильности алгоритмов и программ,
которые могут использоваться для анализа и доказательства правильности других новых алгоритмов и
программ обработки данных.
Общий вывод, который мы хотим сделать, состоит в том, что применение доказательных методов
превращает программирование в научную дисциплину создания безошибочных алгоритмов и надеж-
ных программ для ЭВМ.
Вопросы