2.3.1 Зачем нужны доказательства правильности?

Next:2.3.2 Внешняя спецификация программы
Up:2.3 Доказательство свойств программ
Previous:2.3 Доказательство свойств программ

2.3.1 Зачем нужны доказательства правильности?

Программирование включает в себя не только составление, но и исследование программы, доказательство ее свойств, главным из которых является правильность программы. Здесь речь идет не о синтаксической правильности (она автоматически проверяется транслятором), а о соответствии синтаксически правильной программы той задаче, для решения которой она предназначена. Однако каждый кто сам составлял и/или применял чужие программы отчетливо и с горечью осознает, что в большинстве из них содержатся ошибки.

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

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

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