Правильность алгоритма

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

Доказательство правильности построенного алгоритма не может быть проведено экспериментально, т.е. с помощью прогона программы, реализующий данный алгоритм на различных тестах. Необходимо строгое математическое доказательство правильности.

Вероятно, наиболее распространенная процедура доказательства правильности программы в целом — это прогон ее на разных тестах. Если выданные программой ответы могут быть подтверждены известными или вычисленными вручную данными, возникает искушение сделать вывод, что программа «работает». Однако этот метод редко исклю­чает все сомнения; может существовать случай, в котором программа не сработает. Действительно, практически невозможно в нетривиальных случаях произвести всестороннее и полное ее испытание с целью выявления ошибок. С этой целью целесообразно вспомнить высказывание Э.Дейкстры о том, что экспериментальное тестирование программ может служить доказательством наличия в них ошибок, но никогда не докажет их отсутствие. Естественно поэтому стремление программистов найти возможность формулировать и доказывать некоторые утверждения, касающиеся правильности созданной программы, подобно тому, как в математике формулируются и доказываются, например, теоремы существования и единственности решения. Такие методы возникли и стали весьма интенсивно развиваться в конце 60-х годов.

Идея математического доказательства корректности программ (верификации) обычно сводится к доказательству того факта, что программа (подпрограмма) является корректной относительно ее входной и выходной спецификации. Наиболее известный метод, называемый методом индуктивных утверждений, был предложен в 1967г. Флойдом, хотя сама идея его восходит к Тьюрингу (1950г.).

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

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

Пример. Алгоритм вышерассмотренной задачи (или как его называют алгоритм ETS) настолько прост, что его правильность легко доказать. Поскольку проверяется каждый тур, должен быть проверен и тур с минимальной стоимостью; как только до него дойдет очередь, он будет запомнен. Он не будет отброшен — это может слу­читься только в том случае, если существует тур с меньшей стоимо­стью. Алгоритм должен закончить работу, так как число туров, ко­торые нужно проверить, конечно. Подобный метод доказательства известен как «доказательство исчерпыванием»; это самый грубый из всех методов доказательства.

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