КАТЕГОРИИ: Архитектура-(3434)Астрономия-(809)Биология-(7483)Биотехнологии-(1457)Военное дело-(14632)Высокие технологии-(1363)География-(913)Геология-(1438)Государство-(451)Демография-(1065)Дом-(47672)Журналистика и СМИ-(912)Изобретательство-(14524)Иностранные языки-(4268)Информатика-(17799)Искусство-(1338)История-(13644)Компьютеры-(11121)Косметика-(55)Кулинария-(373)Культура-(8427)Лингвистика-(374)Литература-(1642)Маркетинг-(23702)Математика-(16968)Машиностроение-(1700)Медицина-(12668)Менеджмент-(24684)Механика-(15423)Науковедение-(506)Образование-(11852)Охрана труда-(3308)Педагогика-(5571)Полиграфия-(1312)Политика-(7869)Право-(5454)Приборостроение-(1369)Программирование-(2801)Производство-(97182)Промышленность-(8706)Психология-(18388)Религия-(3217)Связь-(10668)Сельское хозяйство-(299)Социология-(6455)Спорт-(42831)Строительство-(4793)Торговля-(5050)Транспорт-(2929)Туризм-(1568)Физика-(3942)Философия-(17015)Финансы-(26596)Химия-(22929)Экология-(12095)Экономика-(9961)Электроника-(8441)Электротехника-(4623)Энергетика-(12629)Юриспруденция-(1492)Ядерная техника-(1748) |
Правильность алгоритма
Доказательство правильности алгоритма - это один из наиболее трудных, а иногда и особенно утомительных этапов создания алгоритма. Доказательство правильности построенного алгоритма не может быть проведено экспериментально, т.е. с помощью прогона программы, реализующий данный алгоритм на различных тестах. Необходимо строгое математическое доказательство правильности. Вероятно, наиболее распространенная процедура доказательства правильности программы в целом — это прогон ее на разных тестах. Если выданные программой ответы могут быть подтверждены известными или вычисленными вручную данными, возникает искушение сделать вывод, что программа «работает». Однако этот метод редко исключает все сомнения; может существовать случай, в котором программа не сработает. Действительно, практически невозможно в нетривиальных случаях произвести всестороннее и полное ее испытание с целью выявления ошибок. С этой целью целесообразно вспомнить высказывание Э.Дейкстры о том, что экспериментальное тестирование программ может служить доказательством наличия в них ошибок, но никогда не докажет их отсутствие. Естественно поэтому стремление программистов найти возможность формулировать и доказывать некоторые утверждения, касающиеся правильности созданной программы, подобно тому, как в математике формулируются и доказываются, например, теоремы существования и единственности решения. Такие методы возникли и стали весьма интенсивно развиваться в конце 60-х годов. Идея математического доказательства корректности программ (верификации) обычно сводится к доказательству того факта, что программа (подпрограмма) является корректной относительно ее входной и выходной спецификации. Наиболее известный метод, называемый методом индуктивных утверждений, был предложен в 1967г. Флойдом, хотя сама идея его восходит к Тьюрингу (1950г.).
Мы предложим следующую общую методику доказательства правильности алгоритма. Предположим, что алгоритм описан в виде последовательности шагов, скажем, от шага 0 до шага m. Постараемся предложить некое обоснование правомерности для каждого шага. В частности, может потребоваться лемма об условиях, действующих до и после пройденного шага. Затем постараемся предложить доказательство конечности алгоритма, при этом будут проверены все подходящие входные данные и получены все подходящие выходные данные. Такое доказательство - наиболее лучшее, однако для программ, которые по сложности стали превосходить любые известные до сих пор рукотворные произведения человека, проверка их правильности часто не может быть реализована теоретическим доказательством. Она заключается прежде всего при их воплощении и испытании. И зачастую, когда невозможно доказать правильность программы теоретически, ошибки выявляются на стадии тестирования и последующей эксплуатации программы. Этот процесс называется сопровождением программного обеспечения. Пример. Алгоритм вышерассмотренной задачи (или как его называют алгоритм ETS) настолько прост, что его правильность легко доказать. Поскольку проверяется каждый тур, должен быть проверен и тур с минимальной стоимостью; как только до него дойдет очередь, он будет запомнен. Он не будет отброшен — это может случиться только в том случае, если существует тур с меньшей стоимостью. Алгоритм должен закончить работу, так как число туров, которые нужно проверить, конечно. Подобный метод доказательства известен как «доказательство исчерпыванием»; это самый грубый из всех методов доказательства. Подчеркнем тот факт, что правильность алгоритма еще ничего не говорит о его эффективности. Исчерпывающие алгоритмы редко бывают хорошими во всех отношениях.
Дата добавления: 2014-12-16; Просмотров: 1863; Нарушение авторских прав?; Мы поможем в написании вашей работы! Нам важно ваше мнение! Был ли полезен опубликованный материал? Да | Нет |