Информатика
Элементы доказательного программирования - часть 9
алг «нахождение минимума»
массив x[1:N]
нач Результаты:
от k = 1 до N цикл
тп := x[k] mnk = { x[k], при x[k] < mnk-1,
все { mnk-1, в ином случае
кцикл [ k = (1 ... N)]
Min := тп Min = mnN
кон
Утверждение. Приведенный алгоритм определения минимального значения последовательности чисел неправильный.
Доказательство. Для демонстрации ошибок необходимо привести контрпример. Для построения контрпримера разберем результаты выполнения на первом шаге цикла.
Результаты выполнения первого шага цикла при k = 1:
mn1
= = min (х[1], mn0).
mn0
при х[1] £
mn0
Следовательно, результатом будет
mn1 = min (x[l], mn0)
Однако поскольку начальное значение mn0 неизвестно, то неопределено значение результата выполнения первого шага цикла. Аналогичное утверждение можно сделать о втором и всех последующих шагах выполнения цикла:
mnk
= min (x[k], Min(x[k-l], ..., х[1], mn0) = Min (x[k], x[k-1], ..., х[1], mn0).
В силу математической индукции это утверждение справедливо при k = N:
mnN
= Min (x[N], x[N - 1], ..., x[2], х[1], mn0),
Таким образом на основании этого утверждения можно сделать заключение о конечном результате выполнения алгоритма в целом:
Min = mnN
= Min (x[N], x[N - 1], ..., x[2], х[1], mn0).
Из этой формулы видно, что конечный результат равно как и результат первого присваивания зависит от начального значения mn0 переменной mn. Однако эта величина не имеет определенного значения, соответственнно неопределен и конечный результат выполнения алгоритма в целом, что и является ошибкой.
В самом деле, если значение mn0 окажется меньше любого из значений последовательности х[1], ....
