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

Проверка правильности программного обеспечения, как уже говорилось, не является единственной задачей, стоящей перед специалистами в области вычислительной техники. Также важной является проверка аппаратного обеспечения, которое выполняет программу, на отсутствие дефектов. Этот процесс включает в себя проверку работы как отдельных схем, так и всей машины. Проверка современной техники основывается на тестировании. Это означает, что в конечном продукте могут проявиться неявные ошибки. Например, машина Mark I, созданная в Гарвардском университете в 40-х годах XX века, содержала ошибки, которые не проявлялись в течение многих лет. В качестве другого примера можно привести дефект представления чисел с плавающей точкой в ранних микропроцессорах Pentium. В обоих случаях ошибка была обнаружена прежде, чем она привела к каким-либо серьезным последствиям.

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

Первое утро: отдать одно кольцо.

Второе утро: забрать одно кольцо и отдать цепочку, состоящую из двух колец.

Третье утро: отдать одно кольцо.

Четвертое утро: забрать три кольца и отдать цепочку, состоящую из четырех колец.

Пятое утро: отдать одно кольцо.

Шестое утро: забрать кольцо и отдать цепочку, состоящую из двух колец.

Седьмое утро: отдать кольцо.

Следовательно, первый ответ, который мы считали правильным, не является таковым. Можно ли быть уверенным, что наше новое решение правильно? Будем рассуждать так: поскольку в первое утро нужно отдать одно кольцо, то по крайней мере одно кольцо должно быть разрезано. А так как наше новое решение предполагает, что будет разрезано только одно кольцо, то оно является оптимальным.

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

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

Так же как формальное математическое доказательство основывается на аксиомах (например, доказательство в геометрии часто проводится с помощью аксиом Евклидовой геометрии), формальное доказательство правильности программы основывается на характеристиках программы. Для того чтобы доказать, что программа правильно сортирует список имен, нужно начать с предположения, что входные данные программы — это список имен; или, если программа вычисляет среднее нескольких положительных чисел, мы предполагаем, что входными данными являются несколько положительных чисел. Говоря проще, доказательство правильности программы начинается с предположения, что в начале выполнения программы имеют место некоторые условия, которые называются предварительными условиями (preconditions), или предусловиями.

Следующий шаг в доказательстве правильности — посмотреть, как эти предусловия меняются в процессе выполнения программы. Исследователями были проанализированы различные операторы, чтобы посмотреть, как выполнение оператора влияет на истинность утверждения. Например, если до выполнения команды X<-Y было сделано некоторое утверждение о переменной Y, тогда после выполнения программы то же самое утверждение является истинным для переменной X. Говоря более точно, если значение переменной Y не равно 0 до выполнения команды, то можно сделать вывод, что после выполнения команды значение переменной X не будет равно 0.

Вот более сложный пример с оператором i f:

if (условие) then (команда 1)

else (команда 2).

Здесь, если некое утверждение истинно до выполнения оператора, то непосредственно перед выполнением команды 1 известно, что это утверждение и проверяемое условие истинны, а если выполняется команда 2, то истинными являются утверждение и отрицание проверяемого условия.

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

В качестве примера рассмотрим оператор цикла while (рис. 4.16). Предположим, что в результате заданных в точке А предусловий некоторое утверждение истинно всегда, когда происходит проверка условия завершения (точка Б). Такое утверждение называется инвариантом цикла (loop invariant). Затем, если выполнение цикла, завершается, программа переходит к точке В, в которой и инвариант цикла и условие завершения истинны. (Инвариант цикла является истинным, так как проверка условия завершения не изменяет значений переменных программы; условие завершения является истинным, так как в противном случае выполнение цикла не было бы завершено.) Если эти утверждения совпадают с предполагаемыми выходными данными, то доказать правильность можно, просто показав, что выполнение шагов инициализации и модификации в конце концов приводит к условию завершения.

Вспомним наш пример алгоритма сортировки методом вставки (см. листинг 4.2). Внешний цикл этой программы имеет следующий инвариант цикла:

Каждый раз. когда проверяется условие завершения, имена, предшествующие N-му элементу, являются упорядоченным списком.

А условием завершения является следующее утверждение:

Значение N больше длины списка.

Следовательно, если выполнение цикла завершается, то оба этих условия должны быть истинными, то есть весь список должен быть отсортирован.

К сожалению, формальные методы проверки правильности программ не разработаны настолько хорошо, чтобы их можно было с легкостью применять к общим прикладным задачам. В результате в настоящее время в большинстве случаев программное обеспечение проверяется посредством тестирования его при различных условиях, что очень ненадежно. Кроме того, проверка путем тестирования доказывает только то, что программа работает правильно в случаях, предусмотренных тестированием. Любые дополнительные умозаключения — просто предположения. Ошибки, которые содержит программа, часто являются результатом неявных дефектов, которые нелегко заметить в процессе тестирования. Следовательно, ошибки в программе, так же как наша ошибка в задаче с золотой цепочкой, могут остаться незамеченными, часто это так и происходит, даже если значительные усилия были потрачены на то, чтобы избежать их. В качестве примера можно привести случай с компанией AT&T: ошибка в ее программном обеспечении, управляющем 114 телефонными станциями и установленном в декабре 1989 года, была незаметной до 15 января 1990 года, когда сложившиеся условия привели к тому, что было заблокировано около 9 миллионов звонков.