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

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

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

Для сложных программ удачное тестирование не дает гарантии того, что программа не содержит ошибок.

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

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

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

Более строгий путь проверки программы – верификация, которая представляет собой теоретическое обоснование правильного вычисления программы и включает логико-математическое доказательство того, что вычислительное поведение программы правильно.