Т. Пратт, М. Зелковиц - Языки программирования - разработка и реализация (4-е издание_ 2002) (1160801), страница 48
Текст из файла (страница 48)
Программист, разумеется, знает, какую функцию программа должна вычислять, Предположим, что в программу отдельно встроена спецификация этой функции. Предположим также, что по виду программы мы в состоянии определить, какую функцию она вычислила на самом деле. Если бы мы могли показать, что программа в действительности вычисляет точно определенную функцию, то и без тестирования это было бы достаточным доказательством корректности программы. Исчисление лредикатов — это система обозначений в формальной логике, которая полезна, в частности, для точного определения сложных функций.
Разработано несколько подходов к доказательству корректности программ, основанных на предположении, что функция, вычисляемая программой, определена с помощью исчисления предикатов, Программа исследуется на предмет соответствия вычисляемой ею функции той, которая задана с помощью формулы исчисления предикатов. Обычно используется следующее обозначение: (Р)5(0). Смысл его в том, что если предикат Р истинен до начала выполнения оператора 5 и если последний выполняется и завершается, то после выполнения оператора 5 истинным будет и предикат О.
Дополнив это обозначение несколькими правилами вывода, мы можем встроить эту структуру в систему доказательств на основе исчисления предикатов, как показано в следующей таблице. 4.2. Семантика языка 171 Правило Предпосылка Следствие (Р(ехрг))х :- ехрг(Р(х)) (Р) Н В Хвеп 51 е1ве 5г(О) (Р) хоппе В бо 5(Рл В) 4. Присваиеание В.Условие 6. Цикл хгИе х:-ехрг (РлВ)51(0),(Рл В)5г(0) [РлВ)5(Р) Листииг4.1. Программадля вычисления у = А х В (В>0) 1, Мвгт(Д,В) л ( 2 а =А. 3. Ь:-В 4.
у -О, 5, вгл1е Ь>0 бо Ьешо 6. У:=У>а: 7. Ь;=Ь-1: елб) (у = дхВ) В примере 4.1 содержится доказательство правильное~и программы МОЬТ, кото- рая вычисляет у = А х В. При изучении программы можно увидеть, что на каждом шаге цикла лм11е к У добавляется а, в то время как произведение а х Ь уменьшает- ся на з за счет уменьшения Ь па 1. Следовательно, в данном случае ннвариантом является у + а х Ь = А х В У Ь > О, Если удастся показать, что предпосылка в данном правиле вывода истинна, то можно заменить ее следствием. Это позволяет строить доказательства правильности программ в пределах известной нам концепции исчисления предикатов. Аксиоматическая верификация обычно проводится в обратном порядке по отношению к ходу выполнения программы. Зная результат выполнения какого-либо оператора (постусловие), мы можем вывести, какое предусловие должно быть истинно, до начала выполнения етого оператора.
Например, если постусловием для оператора присваивания Х:= У > 2 является Х > О, то, согласно аксиоме присваивания: (Р(ехрг))х .= ехрг(Р(х)) где Р(х) = Х > О, мы получаем (Х>2>0)Х := У + 2(Х > 0). Таким образом, предусл ови ем для нашего оператора присваивания должно быть 1+ 2 > О. Продолжая втомжедухе,мыможемдоказатькорректность(ноуженес такой легкостью) последовательности операторов, содержащей операторы присваивания, условия (11) и цикла (ьм11е). Возможно, наиболее интересным является правило вывода для оператора цикла лм11е: 11 (РлВ)5(Р) ГЬЕЛ (Р) НМ 1Е В бе 5(Рл В). Предикат Р обычно называется инеарианточ, он должен быть истинным и до начала цикла нм11е, и по его окончании.
Хотя для отыскания инвариантов существуют звристические методы, но в целом эта проблема не имеет решения (см. раздел 4.1.3). Тем не менее для многих корректных программ инварианты можно определить. 172 Главал. Моделирование свойств языка Условие (Г)5(0) означает, что если 5 завершится и Р истинно перед началом выполнения 5, то 0 будет истинным по окончании 5. Для оператора присваивания и условного оператора ~(здесь не возникает проблем. Оба они должны завершится. Но для оператора вп11е это не всегда так: нужно еще доказать, что цикл завершится. Обычно используется следующий метод: 1.
Сначала следует показать, что существует некая целочисленная функция 1; такая что в процессе выполнения цикла эта функция остается положительной,у'>О. 2, Еслибы, — это значение функцнну во время 1-го выполнения цикла, то/,., < 1» Если оба условия выполняются, то такой цикл должен завершиться (см. задачу 8 в конце этой главы). Рассмотренная система будет полезной па практике только в том случае, если удастся автоматизировать процесс доказательства корректности программы; применение к реальным программам методов доказательства, предложенных в этой главе, требует массы достаточно утомительных вычислений.
Ошибка в доказательстве может привести к выводу, что программа корректна, в то время как это, возможно, не так. По этим причинам желательно автоматизировать процесс доказательства таким образом, чтобы на основе функционалыюй спецификации программы и самой программы автоматическая система доказательства могла без участия (или с минимальным участием) программиста доказать ее корректность. В настоящее время методы доказательства правильности программ счи~аются полезными, если их можно применять уже на стадии проектирования программы, то есть чтобы программу можно было исследовать на корректность по мере ее написания. Оказалось, что если программа была написана обычным образом, то есть не структурирована специально для облегчения проверки корректности, ее очень трудно или даже невозможно проверять автоматически. Методы автоматической проверки корректности иногда бывают полезны, но они являются недостаточно мощными, чтобы взаимодействовать с чрезвычайно сложными структурами, которые встречаются в более старых, неоднократно модифицированных программах.
Методы доказательства корректное~и программ обычно преподаются програмл~истам-практикам, а также рассматриваются в различных вводных курсах по программированию. Исследования в атой области повлияли на идеологию новых языков программирования. При возможности выбора разработчики языка отдают предпочтение тем свойствам, которые не препятствуют применению методов доказательства правильности программ, и пытаются избегать тех свойств, которые затрудняют это доказательство.
Например, были проведены исследования, показавшие, что следует избегать включения в язык возможности создания псевдонимов имвн, так как это препятствует доказательству корректности программ на этом языке (см. раздел 9 2.1), В некоторые языки, например в С н-, включен специальный макрос э эзегц возможности которого основаны оз части на описанном аксиоматическом методе (см.
раздел 11.1.1). С помощью этого макроса в текст исходной программы вставляется некое утверждение, которое «тестируется» во время выполнения программы. Подобный подход не является априорным методом доказательства корректности программы, но вставка утверждения в текст программы позволяет обнаружить множество ошибок, которые проявляются цри дальнейшем ее использовании. 4.2.
Семантика языка 173 Пример 4.1. Аксиоматическое доказательство правильности программы МЦ1 Т Обычно доказательство происходит в обратном порядке по отношению к ходу выполнения программы, то есть предпосылка выводится из следствия. Нам необходимо найти инварианты для цикла иь()е (строки 5 — 7 листинга 4.1): у увеличивается на 1, в то время как Ь уменьшается на 1, Тогда инвариантом является (у + аЬ = АВ) л (Ь > О) Основание Оператор (у + а(Ь - 1) - АВ и (Ь - 1 » О) ь =ь- Ну ° аь=явль>а» [у ~ аЬ=ЯВлЬ -1>о)у =у а (У '- а(Ь - 1) = АВ л Ь - 1 > О) (У + аЬ = АВ л Ь - 1 > а) у:=ука;Ь =Ь-1 (у + аЬ = Ав л Ь > О) (у ~ аЬ =.
АВ) л (Ь > 0) и Ьь > О) > (у + аЬ = АВ) л Ь - 1 > О (у + аЬ = АВ л (Ь > 0) и (Ь > О)) у.-у>а.Ь =.Ь-1 [у ° аЬ=ЯВ> Ь>0) (у к аЬ - АВ п (Ь > 0))ъчЫв". (у > аЬ = АВ и Ь > О л Ь >О) (О а аЬ = АВ л Ь в О) у; = О(у + аь = Ав л Ь В 0) (О к аВ = АВ и В > О] Ь .=. В [а > аЬ - яВ л Ь> а) (О + Яв = АВ л (В > 0))а .- А (О + аВ = АВ л В> 0) В>0 ааЯВ-ЯВпВ>0 (В > О)а .= А(а > яВ = ЯВ л В > О) (В > 0) а = Я Ь = В, у .= а [у к аЬ = ЯВ л Ь > О) [В > 0) ИОЬТ(А,В) [У + аЬ = ЯВ л Ь а О Ь О) (у + аЬ = АВ) и (Ь > 0) и (Ь > О) ~ (Ь 0) л (У = ЯВ) (В > О) Наьт(я.в) (у = АВ) Правило присваивания (строкв 7) Правила присваивания (строкв 6) Правило композиции (в, Ь) Теорема Правило консвквенцииг (с, С) Правило цикла им )е (строкв 5, в) Правило присваивания (строка 4, () Правило присваивания (строка 3, О) Правило присваивания (строкв 2, Ь) Теорема Правило консвкввнциик Правило композиции (К, Ь, С) Правило композиции (), () Теорема Правило консвкввнции,(т,п) Также нужно показать, что программа завершит свое выполнение.
Достаточно показать, что должны завершиться все циклы иь()е. Обычный способ таков. 1. Показать, что существует некоторое свойство, которое всегда положительно во время выполнения цикла (например, Ь > О). 2. Показать, что при последовательных итерациях цикла зто свойство уменьшается (например, Ь:= Ь вЂ” 1). Если оба свойства остаются истинными, то цикл должен завершиться. 1т4 Глава 4. Моделирование свойств языка 4.2.5. Алгебраические типы данных Операции перезаписи членов и унификации, огшсанные нами ранее, играют важную роль в развитии модели алгебраических типов данных.
Если мы описываем отношения между рядами функций, то мы констатируем, что любая реализация, согласованная с этими отношениями, является корректной реализацией. Например, стек (атаев), содержащий целые числа, можно определить с помощью следующих операций: раап : Маса х 1пседе~ а маса рор: агась -а маса гор : агасх -а 1пгедег су (иппе11пеп~ евргу : агасх -а Воо1еап 51ае асаса -а |пседег пеиагасх -> агась Операции розп и рор здесь используются в своей обычной интерпретации, сор возвращает верхний элемент стека, не удаляя его, евргу проверяет, не является ли стек пустым, з1ае возвращает количество элементов в стеке и пензсасх создает новый экземпляр стека.
Генерирование алгебраических аксиом Пусть существует множество операций, определяющих тип данных. Мы можем привести некоторые эвристические соображения для построения взаимоотношений между этими операциями. Операции разделяются на три класса: генераторы, конструкторы и функции. Генераторы. Для абстрактного типа данных х генератор д создает новый экземпляр этого типа. Следовательно, его сигнатурой будет д : пег х -а х (пес х обозначает любой тип данных, отличный от х).
В нашем примере со стеком генератором является операция пена'саФ. Конструкторы. Конструкторы с модифицируют экземпляры абстрактного типа х и имеют следующую сигнатуру: с: х х пот х -> х Примером конструктора являешься операция розП. Функции. Все остальные операции над данными абстрактного типа х относятся к функциям. В нашем примере со стеком функциями являются гор, рор, зтае и епргу Интуитивно понятно, что любой объект у абстрактного типа х создается посредством применения генератора и повторного применения конструкторов. Для стеков это означает, что любой стек является результатом использования генератора пеизгас1, который создает пустой стек, и последовательного применения оператора ркиб для помещения в стек каких-либо объектов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
