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