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

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

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

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

рис. 4.1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Большинство последних работ, где проблемы построения программ связываются с проблемами их правильности, посвящены структурному программированию. Основное внимание в них уделяется таким методам создания программ, которые позволяли бы программисту следить (неформально убеждаться) за правильностью программы на всех этапах процесса программирования. Этой теме посвящены работы Дейкстры и Хоара «структурное программирование», а также работа Макхована и Келли «Стратегии структурного программирования «сверху вниз» и «снизу вверх». Вирт в книге «Системное программирование: введение» написал введение в программирование, где он так же рассматривает структурное программирование и проблемы доказательства правильности. В работе Хоара «Доказательство правильности структурированных программ» приводится детальное доказательство правильности для одной структурированной программы. Миллс («Новые пути компьютерного программирования» и «Как написать правильную программу и доказать это») и Бакер («Структурное программирование в создании программного обеспечения») рекомендуют использовать структурное программирование при создании программного обеспечения. Проблемы структурного программирования и использования оператора перехода рассматриваются и в работе Кнута «Структурное программирование с оператором go to».