Доказательство правильности программ (стр. 7 )

F(N) = IF N = 0 ТНЕN 1

ЕLSЕ ОТНЕRWISЕ 2 • F(N – 1),

выведите формулу для вычисляемой функции F(N) и докажите ее правильность.

4.3. Структурная индукция для нерекурсивных программ

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

Пример 4.9. Мы хотим доказать, что если выполнять программу, блок-схема которой приведена на рис. 4.1, с TREE, представляющим собой указатель на корневую вершину некоторого двоичного дерева (TREE = L, если дерево пустое), то в конце концов выполнение ее закончится, причем будут просмотрены в некотором порядке все вершины этого дерева. (Для ознакомления с используемой в блок-схеме нотацией и алгоритмами просмотра двоичных деревьев см. стр. 394-398 в книге Д Кнута «Искусство программирования для ЭВМ», том 1, изд-во «Мир», 1976.) Просмотр идет следующим образом: для каждой вершины дерева просматриваются одним и тем же способом все вершины левого поддерева, выходящего из данного, затем сама исходная вершина, а затем в том же порядке все вершины правого поддерева. Наша программа фактически реализует некоторый рекурсивный процесс, и ее можно было бы легко написать в «рекурсивной форме». В нашей же нерекурсивной версии алгоритм основан на использовании явного стека. Мы могли бы доказать, что программа правильна, и методом индуктивных утверждений (студенты могут проделать это самостоятельно в качестве упражнения), однако рекурсивность самого процесса приводит к предположению, что это доказательство удобнее провести с помощью структурной индукции. Сначала докажем, что справедливо утверждение, связанное в блок-схеме с точкой 2. При доказательстве используется структурна, индукция по размеру (числу вершин) дерева, на которое указывает Р. Для этого необходимо:

1. Доказать, что если размер дерева, на которое указывает Р, равен нулю, то утверждение справедливо. Но если размер дерева, задаваемого Р, равен нулю, то наше утверждение тривиально, ибо мы попадаем в точку 2 с пустым деревом, которое можно считать уже просмотренным в соответствующем порядке (ведь просматривать нечего), причем Р = L, а SТАСK остался без изменений.

2. Доказать (для всех n > 0), что если наше утверждение верно для всех деревьев размером меньше n (гипотеза индукции), то оно также справедливо и для дерева размером n. Предположим, что мы находимся в точке 2 и Р = Р0 = L, затем переходим из точки 2 через точки 3, 4 вновь в точку 2.

рис. 4.1

При возвращении в точку 2 Р указывает на левое поддерево первоначального дерева, на которое указывало Р (т. е. Р = LLINK(Р0)), а SТАСК в состоянии 5ТАСК0,Р0 (т. е. значение Р0 уже помещено в вершину стека). Так как размер дерева, на которое теперь указывает Р, меньше n, то мы знаем (по гипотезе индукции), что если мы когда-нибудь вернемся в точку 2, то это левое поддерево уже будет просмотрено в соответствующем порядке и, кроме того, Р = L, а SТАСК опять будет в состоянии SТАСК0,Р0. Так как Р = L, пройдем по пути из точки 2 через точки 6, 7, 8 вновь в точку 2. Вернувшись в точку 2, будем иметь Р = PLINK(Р0), а SТАСК – в состоянии SТАСК0. Исходная вершина будет уже просмотрена. Таким образом, уже будут просмотрены в соответствующем порядке вершины левого поддерева и корень (исходная вершина) дерева. Указатель Р теперь будет «смотреть» на правое поддерево; оно меньше дерева, на которое указывал Р0. Опять можно использовать гипотезу индукции и сделать заключение, что, если в конце концов мы вернемся в эту точку, дерево, на которое указывает Р, будет просмотрено (это правое поддерево исходного дерева), Р = L и SТАСК будет в состоянии SТАСК0. В этот момент оказывается, что мы просмотрели левое поддерево, корневую вершину и правое поддерево. Но из этого следует, что мы в соответствующем порядке просмотрели все исходное дерево. Причем Р = L, а SТАСК – в состоянии SТАСК0, что и требовалось доказать.

Изложенное доказательство легко приводит нас и к доказательству правильности, так как при первом попадании в точку 2 (из точки 1) Р = ТRЕЕ, а SТАСК пуст. Только что доказанное утверждение, связанное с точкой 2, гласит, что при попадании в точку 2 поддерево, на которое указывал Р, будет уже надлежащим образом просмотрено и SТАСК будет в исходном состоянии (пуст), а Р = L. В этот момент, так как Р = L, мы попадем в точку 5, так как SТАСК пуст, далее – в точку 10; это и показывает справедливость утверждения о правильности, связанного с точкой 10.

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

Глава 5. СОВРЕМЕННЫЕ ИССЛЕДОВАНИЯ, СВЯЗАННЫЕ С ДОКАЗАТЕЛЬСТВОМ ПРАВИЛЬНОСТИ ПРОГРАММ

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

1. Методы доказательства (частичной) правильности или конечности.

2. Проблемы разработок программ и создания языков программирования.

3.  Механизация процесса доказательства правильности.

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

5.1. Методы доказательства

В наших учебных пособиях (и в курсе теории вычислительных процессов) мы сконцентрировали внимание на двух основных методах: методе индуктивных утверждений и структурной индукции. Метод индуктивных утверждений впервые был предложен Флойдом и Науром. Барстелл в 1969 г. предложил метод структурной индукции. В главе 2 очень кратко рассмотрены понятия, относящиеся к правилам верификации и аксиомам для доказательства частичной правильности. Этот метод, впервые предложил Хоар.

Существуют и другие методы доказательства правильности программ. Различные методы доказательства полной правильности итеративных программ приводятся в работах Базу, Бурсталла, Дейкстры, Манны и др. В работе Бурсталла рассмотрен алгебраический подход к доказательству правильности. В работах Бурсталла и Вегбрейта обсуждаются методы доказательства правильности программ, использующих сложные структуры или модифицирующие структуру данных. В работах Манны показано, как можно использовать метод индуктивных утверждений для доказательства правильности недетерминированных программ. В работах Ашкрофта, Келлера, Липтона рассматриваются методы доказательства правильности параллельных программ.

Такой метод доказательства, как метод индуктивных утверждений, где речь идет лишь о доказательстве частичной правильности, требует отдельного доказательства конечности итеративных программ. Флойд и Манна использовали вполне упорядоченные (или частично упорядоченные) множества для доказательства конечности. В работе Манны проведено сравнение различных методов доказательства конечности. В работе Сайтеса описаны методы доказательства «чистого» окончания программ.

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

В работе Манны «Математическая теория вычислений» дается некоторый формальный подход ко многим известным методам доказательства правильности программ. Рассмотрены методы доказательства правильности и конечности для итеративных и рекурсивных программ.

5.2. Конструирование программ и языков

Желание создавать программы, для которых было бы легко удостовериться в их правильности, привлекло внимание к проблеме конструирования программ и разработки языков программирования. Работа «Конструктивный подход к проблеме правильности программ» была одной из первых работ, относящихся к проблемам конструирования программ и доказательству их правильности. Другая его работа «Программирование без Goto» также была одной из первых, где вопросы разработки языка связывались с проблемами правильности (речь шла об исключении операторов перехода). Эти же проблемы обсуждались и в других его работах.