Глава 2. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ БЛОК-СХЕМ ПРОГРАММ

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

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

Если бы можно было формализовать доказательство правильности и проводить его абсолютно надежным образом (автоматически доказывающим устройством), то ему можно было бы полностью доверять. В будущем это, возможно, окажется реальным, но не сейчас. Мы рассмотрим лишь неформально построенные доказательства правильности. Опыт проведения таких доказательств показывает, что при этом возрастают наша уверенность в программе и ее понимание, и поэтому доказательства следует выполнять, хотя они и не приводят к полной гарантии от ошибок. Неформальное доказательство правильности можно рассма­тривать как некоторую форму систематической проверки программы за столом, без машины, т. е. того, что всегда делает хороший программист. В этой главе даны основные идеи такого доказательства правильности для программ, пред­ставленных блок-схемами.