3.4 Обоснование алгоритма

Next:3.5 Анализ алгоритма и его сложности
Up:3 Общие рекомендации по выполнению заданий
Previous:3.3 Разработка алгоритма

3.4 Обоснование алгоритма

Строгое математическое доказательство правильности работы алгоритма -- обычно очень трудная задача, главным образом из-за того, что трудно доказать правильность работы циклов и рекурсивных процедур. Вместе с тем демонстрация правильной работы алгоритмов на некотором наборе тестов еще не означает, что он всегда будет работать правильно. Следует помнить, что различных комбинаций входных данных бывает, как правило, бесконечно (или "практически" бесконечно) много. Поэтому необходимо сопровождать алгоритм некоторым рассуждением, которое, даже не будучи строгим доказательством, в достаточно полной мере убеждает нас в правильности алгоритма. Конечно, оно не должно быть рассуждением в таком, например, стиле: "алгоритм перебирает все варианты, поэтому он правилен". Ведь тогда возникает вопрос, а как убедиться, что алгоритм действительно перебирает все варианты.

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

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

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

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

Вставка в программу "стопоров ошибок" (динамических проверок свойств, выраженных в аннотациях) упрощает процесс отладки и позволяет существенно повысить надежность разработанной программы.