Название: Доказательство правильности программ - Конспект лекций (Веретельникова Е.Л.)

Жанр: Экономика

Просмотров: 1604


2.1. введение

 

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

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

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

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