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

Виды алгоритмов

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

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

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

Третий метод известен как отрабатывание назад, т.е. начинаем с цели или решения и движемся обратно по направлению к начальной постановке задачи. Затем, если эти действия обратимы, движемся от постановки задачи к решению.

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

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

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

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

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

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

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

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

Дата добавления: 2014-01-06