 |
 |
 |
 |
|
 |
 |
123
Конструктивно, доказательства правильности алгоритмов и программ строятся на суждениях и
утверждениях о результатах выполнения каждого из составляющих их действий и операций в соответ-
ствии с порядком их выполнения.
В качестве примера проведем анализ результатов алгоритма, состоящего из трех присваиваний.
алг «у = х
5
»
Результаты
Утверждения
нач
v := х
х
v1 = х
х
v1 = x²
v := v
v
v2 = v1
v1
v2 = x
4
у := v
x
у = v2
x
у = х
5
кон
Справа от алгоритма приведены результаты выполнения присваиваний. Результатом первого
присваивания v := х
х будет значение v1 = х
х переменной v. Результат следующего присваивания v :=
v
v - второе значение переменной v, равное v2 = v1
v1 . Результатом третьего присваивания у := v
x будет
значение у = v2
x .
На основе приведенных рассуждений, можно сделать три утверждения о промежуточных и конечных
результатах вычислений:
Результаты
Утверждения
{ v1 = х
х
v1 = х²
{ v2 = v1
v1
v2 = x
4
{ у = v2
x
у = х
5
Таким образом можно высказать окончательное
Утверждение. Конечным результатом выполнения будет
у = х
5
для любых значений х.
Доказательство. Исходя из описания результатов выполнения присваиваний значение у будет равно
у = v2
x = (v1
v1)
x = ((х
х).(х
х)))
х = x
5
.
Что и требовалось доказать.
Техника анализа и доказательства правильности алгоритмов и программ во многом совпадает с
техникой доказательства любых других утверждений и состоит в применении следующих четырех
приемов:
разбор случаев;
подбор контрпримеров;
выделение лемм;
индуктивный вывод.
Разбор случаев применяется для анализа результатов выполнения конструкций альтернативного
выбора. В качестве примера проведем анализ приведенного выше алгоритма «выбора» максимума трех
чисел, содержащего выбор альтернатив.