 |
 |
 |
 |
|
 |
 |
125
mх := b
mх = b
кесли { mх = mах(а,b) }
при с < mх
если с
mх то
при с
mх
mх := с
mх' = с
кесли
кон
Доказательство правильности алгоритмов можно проводить двумя способами. Первый способ -
анализ правильности при построении алгоритмов. Второй способ - анализ правильности после
построения алгоритмов.
Первый способ
- показать, что алгоритм является корректной реализацией метода решения, и
доказать, что метод - правильный. Для рассмотренного алгоритма это доказательство изложено выше.
Привлечение для создания алгоритмов известных методов решения, для которых доказана их
правильность, позволяет существенно упростить обоснование правильности программ. При этом центр
тяжести проблем смещается к созданию и обоснованию гарантированно правильных методов решения
задач.
Второй способ
- исчерпывающий анализ результатов выполнения алгоритма на соответствие
постановке решаемых задач для любых допустимых данных. Это - доказательство путем исчерпыва-
ющего анализа результатов выполнения алгоритмов и программ.
Результаты выполнения рассматриваемого алгоритма вычисления максимума трех чисел приведены
справа от него. Анализ результатов алгоритмов, содержащих конструкцию выбора, требует разбора
случаев. Отметим, что все эти случаи были уже указаны ранее при разборе ошибочной версии
алгоритма.
Для обоснования правильности алгоритма докажем вспомогательное утверждение о результатах
выполнения конструкции альтернативного выбора.
Лемма: Конечными результатами выполнения алгоритма
Алгоритм
Результаты
если а > b то
при а
b
тх := а
mx = a
иначе
при b > a
тх := b
mx = b
кесли
является значение mx = max(а, b) для любых значений а и b.
Доказательство. Результатом вычислений здесь будут значения
а при а
b
mx =
b при а < b
что совпадает с определением max (а, b).
С помощью этой леммы легко доказать правильность алгоритма в целом.
{ mх = max (а, b) }
Результаты
если с
mx то
при с
mx
mx := с
mx' = с
кесли
mx' = mx
при с < mx
Утверждение. Конечным результатом выполнения алгоритма вычисления максимума будет
значение mx' = max (а, b, с) для любых значений а, b и с.
Доказательство. В силу предположения предшествующее значение переменной mx = max(a,b).
Отсюда получаем, что