ВУЗ:
Если следовать правилам, приведенным выше, доказательство корректности программы осуществляется путем опреде-
ления положений, называемых утверждениями, которые устанавливаются в различных точках программы. В результате по-
лучается набор утверждений, каждое из которых является следствием предусловий программы и последовательности инст-
рукций, приводящей к той точке программы, где установлено данное утверждение. Если утверждение, установленное по-
добным образом в конце программы, соответствует спецификациям того, что требуется получить на ее выходе, то можно
сделать заключение о правильности программы.
В качестве примера рассмотрим типичную циклическую структуру while-do, представленную на рис. 4.22. Предпо-
ложим, как следствие предусловий, заданных в точке А, мы можем установить, что определенное утверждение истинно при
каждой проверке условия окончания цикла (точка В) на протяжении всего процесса повторения. Такое утверждение внутри
цикла называется инвариантом цикла (loop invariant). Как только повторение завершается, выполнение переходит к точке С,
где мы можем заключить, что истинны как инвариант цикла, так и условие его окончания. (Инвариант цикла остается истин-
ным, поскольку проверка условия окончания не изменяет никаких величин в программе, а условие окончания истинно, по-
скольку в противном случае цикл бы просто не завершился.) Если комбинация этих положений означает то, что мы хотим
видеть на выходе, наше доказательство корректности можно завершить, просто показав, что компоненты инициализации и
модификации цикла в конечном счете приводят к условию окончания.
Этот метод анализа можно применить к приведенному выше алгоритму сортировки методом вставки (см. рис. 4.11).
Внешний цикл в этой программе основан на следующем инварианте цикла:
Каждый раз при выполнении проверки условия окончания цикла имена, предшествующие N-му элементу, образуют от-
сортированный список.
Рис. 4.22. Использование формального утверждения для проверки
правильности оператора цикла while-do
Условие окончания этого цикла формулируется следующим образом:
Значение N больше, чем длина списка.
Таким образом, как только цикл завершится, мы будем знать, что оба условия должны быть выполнены, а это означает,
что весь список будет отсортирован.
К сожалению, методы формальной верификации программ не настолько хорошо разработаны, чтобы их можно было
использовать в приложениях общего типа. Сегодня в большинстве случаев "верификация" программного обеспечения про-
изводится посредством его тестирования при различных исходных условиях, что весьма ненадежно. Верификация с помо-
щью тестирования не доказывает ничего иного, кроме того, что программа правильно работает в тех условиях, в которых ее
проверяли. Любые дополнительные заключения – это всего лишь предположения. Ошибки, содержащиеся в программе, ча-
ще всего являются следствием оплошности и недосмотра, что может произойти и при тестировании. В результате ошибки в
программе, такие, как в задаче с золотой цепочкой, могут остаться и часто остаются незамеченными, хотя были потрачены
значительные усилия, чтобы этого избежать. Драматический случай произошел в компании AT&T. Ошибка в программном
обеспечении, управляющем 114 телефонными станциями, оставалась незамеченной с момента его установки в декабре 1989
г. и вплоть до 15 января 1990 г., когда исключительное стечение обстоятельств привело к тому, что за девять часов было
беспричинно заблокировано примерно 5 миллионов телефонных звонков.
Вопросы для самопроверки
1. Предположим, было установлено, что при использовании алгоритма сортировки методом вставки машине требуется в
среднем одна секунда для сортировки списка из 100 элементов. Оцените, сколько времени ей понадобится для сортировки
списков из 1000 и 10 000 элементов?
Страницы
- « первая
- ‹ предыдущая
- …
- 100
- 101
- 102
- 103
- 104
- …
- следующая ›
- последняя »
