Cтраница 3
Представление формального аппарата для выражения и передачи идеи проекта является основным в структурном программировании. Формальное описание проекта программы способствует снижению ее сложности и уменьшению усилий на доказательство правильности программы, а также создает основу для пошагового совершенствования программы. [31]
С этой точки зрения, разумеется, весьма желательно превращение программирования в науку, и за 15 лет, прошедшие со дня публикации тех замечаний, которые я процитировал в начале своей лекции, мы несомненно проделали немалый путь в этом направлении. Пятнадцать лет назад мы настолько плохо понимали, что такое программирование, что даже помыслить не могли о доказательствах правильности программ; мы просто-напросто гоняли программу до тех пор, пока не убеждались, что она работает. В те времена мы не представляли даже, как достаточно строго сформулировать саму идею правильности программы. [32]
Вслед за выбором алгоритма следует обоснование его правильности. Наиболее распространенный способ доказательства правильности программы - это прогон ее на разных тестах. Если выданные программой ответы могут быть подтверждены арифметическими вычислениями, то в этом можно усматривать доказательство. [33]
Автоматизация помогает в подробном анализе больших программ, помогает выявить ошибки, освободить программиста от повторяющейся работы. При поиске ошибок автоматизация помогает в выявлении простых ошибок, позволяет программисту сконцентрировать внимание на сложных задачах проверки. Успешное применение формальных методов доказательства правильности программ также в значительной степени зависит от успехов автоматизации. [34]
Интересно, что по данному вопросу имеется больше литературы, чем по любому другому аспекту надежности программного обеспечения. Настоящая глава представляет собой только частичный обзор этой области; более полную картину можно найти в литературе, перечисленной в конце главы, а также в книгах и статьях, на которые там есть ссылки. В этих работах имеется много доказательств правильности программ, включая алгоритмы сортировки и поиска, простейшие компиляторы, подпрограммы численного анализа, ядра операционных систем и программы редактирования. [35]
Дополнительные сложности возникают из-за ограничений, накладываемых машинной арифметикой, неопределенностью результатов и параллелизмом операций. Очень трудным делом может оказаться и разработка спецификации, согласно которой в дальнейшем будет проводиться верификация программы, дело в том, что невозможно показать правильность самой спецификации в смысле верного отображения замыслов разработчиков. Исследования, связанные с поиском способов доказательства правильности программ, внесли существенный вклад в программотехнику, где благодаря таким исследованиям удалось достичь лучшего понимания структуры алгоритмических языкое, принципов и методов программирования. Кроме того, масштабы практического применения формальных методов доказательства правильности программ постоянно расширяются и приобретают все большее значение. [36]
Рассмотрим доказательство правильности элементарных программ на примерах программ, оперирующих скалярными данными. Структуры типа fordo и case обсуждению не подлежат. Доказательство для структуры fordo было рассмотрено выше, а доказательство для структуры типа case является простым обобщением доказательства правильности программы типа ifthenelse. Доказательство правильности программ, использующих данные в виде массива и непоименованные данные, рассматриваются в следующем разделе. Доказательства удовлетворяют верификационным требованиям, определенным теоремой правильности, и записываются в соответствии с синтаксисом доказательства ( см. разд. Чтобы полнее проиллюстрировать оба систематических метода записи данных в трассировочные таблицы и применение логических правил рассуждения, доказательства записываются со всеми синтаксическими и логическими подробностями. Полная правильность доказывается для каждой программы, за исключением программы типа dowhiledo, при доказательстве которой обнаруживается ошибка в программе. [37]
Рассмотрим доказательство правильности элементарных программ на примерах программ, оперирующих скалярными данными. Структуры типа fordo и case обсуждению не подлежат. Доказательство для структуры fordo было рассмотрено выше, а доказательство для структуры типа case является простым обобщением доказательства правильности программы типа ifthenelse. Доказательство правильности программ, использующих данные в виде массива и непоименованные данные, рассматриваются в следующем разделе. Доказательства удовлетворяют верификационным требованиям, определенным теоремой правильности, и записываются в соответствии с синтаксисом доказательства ( см. разд. Чтобы полнее проиллюстрировать оба систематических метода записи данных в трассировочные таблицы и применение логических правил рассуждения, доказательства записываются со всеми синтаксическими и логическими подробностями. Полная правильность доказывается для каждой программы, за исключением программы типа dowhiledo, при доказательстве которой обнаруживается ошибка в программе. [38]
Однако, если программа благополучно проходит этап трансляции, то это не является указанием на отсутствие ошибок. Поэтому программа, которая транслируется до конца, должна пройти семантический контроль для того, чтобы убедиться в том, что она решает именно ту задачу, которую ей пред-назначено решать. В атом заключается проблема доказательства правильности программ. [39]
Такой подход к доказательству правильности программ называют интуитивным. При использовании такого подхода не принимаются во внимание алгебраические свойства структурированных программ. Однако здесь нашей целью является иллюстрация возможности доказательства правильности программ на естественном языке. [40]
Дополнительные сложности возникают из-за ограничений, накладываемых машинной арифметикой, неопределенностью результатов и параллелизмом операций. Очень трудным делом может оказаться и разработка спецификации, согласно которой в дальнейшем будет проводиться верификация программы, дело в том, что невозможно показать правильность самой спецификации в смысле верного отображения замыслов разработчиков. Исследования, связанные с поиском способов доказательства правильности программ, внесли существенный вклад в программотехнику, где благодаря таким исследованиям удалось достичь лучшего понимания структуры алгоритмических языкое, принципов и методов программирования. Кроме того, масштабы практического применения формальных методов доказательства правильности программ постоянно расширяются и приобретают все большее значение. [41]
Верификация правильности ациклических программ выполняется путем их анализа и замещения. Формулируется лемма о преобразовании итеративных программ в рекурсивные, которая позволяет свести верификацию циклических программ к верификации ациклических программ. Теорема правильности программ обобщает требования верификации для структур языка PDL: приведены формальный и неформальный методы доказательства этой теоремы. Теорема об инварианте дает систематическое средство вывода инвариантов цикла. Описывается метод доказательства правильности программ, основанный на инвариантах. Рассматриваются теоретические методы получения эффективных программ. [42]
Некоторые формы иерархической декомпозиции, с которыми мы встретимся, представляют собой нисходящее управление ( гл. Вероятно, многие знакомы с такими видами формальной иерархической декомпозиции, как поэтапная обработка [11], уровни абстракции [12], иерархия документации [13], нисходящее программирование [14], модульная декомпозиция [15], композиционное [16] и структурное [17] проектирование. Александер [18] предлагает весьма интересное представление декомпозиции. В небольшой, но очень полезной книге он проводит философское обсуждение процессов анализа и синтеза конструкций, за которым следует математический метод разложения множества ограничений на подмножества, приводящий к минимизации их взаимодействия. Его работы и работы Бема [19], Хоара [20], Милза [21], а также некоторые пока еще не опубликованные работы представляют собой значителньый вклад в проектирование программного обеспечения благодаря введению количественной меры оценки этого процесса и средствам доказательства правильности программ. [43]
В этом множестве отсутствует структура, соответствующая оператору безусловного перехода GOTO. Правомерность исключения такой структуры будет обоснована ниже при доказательстве теоремы о структурировании, в которой утверждается, что с помощью управляющих структур языка PDL может быть реализована управляющая структура обработки данных любой сложности. В процессе доказательства теоремы о структурировании удается производить систематическое преобразование программ, выраженных в виде произвольных управляющих структур, в эквивалентные программы, представляемые с помощью управляющих структур языка PDL. Простые программы, в том числе и программы на языке PDL, имеют один вход и один выход; поэтому их действие на данные может быть оценено по состоянию на входе и выходе. Элементарные программы - это простые программы, составленные из управляющих структур PDL, которые в определенном смысле ( обсуждаемом ниже) являются неделимыми. Программные функции являются точными и исчерпывающими описаниями действия простой программы на данные - от исходного состояния данных до их конечного состояния. Программные функции играют важную роль при чтении, написании и доказательстве правильности программ. [44]
Следует обратить внимание на то, что доказательство общей правильности программы проводится не путем анализа результатов ее прогона, а на основе анализа программы, как статического математического объекта, на который распространяются аксиомы и правила логического вывода. Основной проблемой доказательства правильности программы является формирование вспомогательных утверждений. Для этого требуется тщательный учет структуры программы и семантики языка программирования. Построения вспомогательных утверждений для некоторой произвольной программы зачастую оказываются очень сложной и конструктивной задачей, поэтому определенные преимущества достигаются тогда, когда процедуры доказательства и правильности программы разрабатываются в процессе ее проектирования. Чтобы доказать факт завершения работы программы, необходимо доказать, во-первых, что программа не остановлена преждевременно, и, во-вторых, что программа не зациклилась. Подтверждение первого факта может оказаться очень сложным, например, может возникнуть потребность в доказательстве того, что не будет происходить арифметического переполнения. Подтверждение того, что программа в конце концов выйдет из некоторого цикла, может быть основано на концепции вполне упорядоченного множества ( W. Допустим, например, что применительно к некоторому циклу выражение Е может быть найдено так, что если оно отрицательно, цикл немедленно завершится. Далее допустим, что может быть доказан факт уменьшения Е с каждой итерацией цикла. Из этого следует, что цикл должен завершиться. Доказательство правильности программы не дает полного решения проблемы надежности программного обеспечения практически используемых систем. [45]