Информатика


Элементы доказательного программирования - часть 6


Для рассмотренного алгоритма это доказательство изложено выше.

Привлечение для создания алгоритмов известных методов реше­ния, для которых доказана их правильность, позволяет существенно упростить обоснование правильности программ. При этом центр тяжести проблем смещается к созданию и обоснованию гарантиро­ванно правильных методов решения задач.

Второй способ - исчерпывающий анализ результатов выпол­нения алгоритма на соответствие постановке решаемых задач для любых допустимых данных. Это - доказательство путем исчерпыва­ющего анализа результатов выполнения алгоритмов и программ.

Результаты выполнения рассматриваемого алгоритма вычисления максимума трех чисел приведены справа от него. Анализ результатов алгоритмов, содержащих конструкцию выбора, требует разбора случаев. Отметим, что все эти случаи были уже указаны ранее при разборе ошибочной версии алгоритма.

Для обоснования правильности алгоритма докажем вспомогатель­ное утверждение о результатах выполнения конструкции альтерна­тивного выбора

Лемма: Конечными результатами выполнения алгоритма

Алгоритм                                          Результаты

если а > 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 и с.




Начало  Назад  Вперед



Книжный магазин