Т. Пратт, М. Зелковиц - Языки программирования - разработка и реализация (4-е издание_ 2002) (1160801), страница 49
Текст из файла (страница 49)
Например, стек, содержащий цифры 1, 5, 3, может быть получен следующим образом: роайроаМроаП(пееаасл, 1). Вк 3) Хотя не существует формальной модели разработки алгебраических аксиом, с успехом применяется следующий эвристический подход. Генерируется аксиома для каждой функции с каждым конструктором и генератором. Поскольку в нашем примере со стеком имеются три функции, один конструктор и один генератор, то 4.2. Семантика языка 175 у нас получается шесть аксиом. Если уже написана левая часть выражения для аксиомы, ее значение (правую часть выражения) обычно легко определить. Например, для функции гор и конструктора риз)) аксиома выглядит следующим образом; гор(роай(5.
1)) - ... Интуитивно ясно, что верхним элементом стека должен быть тот, который только что добавлен, поатому аксиома получается такая: (ор(рить(5, П > = 1 Продолжая в том же духе, мы получим следующие аксиомы: 1. Рор(пеиагаск> = пеиагаск 2: рор(роли(5, 1) - 5 3 Сор(пеиагаск> = ипаен пей 4, Гор(риащ5, 1> = 1 5: еир(у(пека(ась> - ггие б пирсу(роЖ5. 1> = (а)ае 7; ю ге(пеиагасг) = 0 8 юге(риащ5. 1) = юге(5) г 1 Эти аксиомы часто называются правилами перезаписи, при помощи которых можно перезаписать экземпляр какого-либо объекта в более простом виде.
Согласно приведенной спецификации, операция ризй возвращает экземпляр стека (5Оасг), сконструированного из уже имеющегося стека и некоторого целого числа. Например, запрос может быть сформирован как выполнение операции пеизсаск, затем риз)) и еще раз ризй, затем рор и, наконец, выполнение функции еп)рту: юр(у(рор(риал(риащпеиагасх, 42) 17) > Уг)ификация этого выражения при помощи аксиомы 2 позволяет упростить его за счет сокращения рор и рцэй — противоположных по своему действию операций, следующих друг за дру гол(. Тогда выражение принимает следующий вид; еир(у(риал(пека(ась.
42>)) Теперь мы можем использовать аксиому 6 и упростить это выражение до 1а15е. Нам удалось модифицировать выражение таким образом, что функция еа)рту применяется только к суперпозицни конструктора и генератора и выдает значение 1а)эе. Это является иллюстрацией к нашему рассказу о конструкторах, Алгебраическое выражение, состоящее только из генераторов и конструкторов, называется канонической, нли нормальной, формой выражения. Индукция типов данных Пусть дан набор аксиом сто есть отношений) между множеством операций алгебраического типа данных.
Часто требуется проверить истинность определенных свойств. Затем зти свойства становятся обязательными для всех программ (например, на С или на Рааса)), реализующих данную спецификацию. И>гдукг(ия типов данных — это один из способов проверки подобных свойств, Он тесно связан с методом математической индукции. Пусть Р(у) — некий предикат, связанный с у е х. При каких условиях Р всегда будет истинец для любых членов типа х? Как и в случае математической индукции, можно доказать, что Р будет истинно для любых элементарных объектов этого типа'. Помог бктм математической иилукиии.
— Примеч науч Ред. 176 Глава4. Моделирование свойств языка Затем мы можем показать, что при конструировании новых объектов того же типа из элементарных наше свойство Р по-прежнему остается истинным. Индукция типом данных определяется следующим образом. 1. Имеется тип данных х с генераторами Гп конструкторами д„другиии функ- цняМИ Пп а таКжЕ ПредИКат Р(у) дпя у Е Х. 2.
Нужно показать, что Р((,) истинно. Это является базой индукции для доказательства — значение прсдиката на функциях-генераторах истинно. 3, Предположим, что Р(у) истинно. Нужно показать, что из этого следует истинность Р(д,(у) ). Тогда можно расширить предикат Р на все объекты, созданные посредством применения генератора и последуюп(его применения конструкторов.
4. Тепсрь можно сделать вывод, что Р(у) истинно для всех у, принадлежащих типу х. Для нашего примера со стеком нужно показать, что прсликаты Р(пеивгасХ) и Р(рцвл(х, 1) ) истинны. Используя индукцию типов данных, можно показать, что добавление в стек нового объекта увеличивает размер стека, то есть вяге(ропп(5. х)) > юге(5) Доказательство этого утверждения вы найдете в примере 4.2. ПРИМЕР 4.2. Индукция типов данных 1. Для доказательства иСтинноСти пРедиката Р(5) > ваге(раап(5.Х)) > 5)ге(5) мы преобразуем его при помощи аксиом, которые будут применяться до тех пор, пока дальнейшее его упрощение не стане~ невозможно: и ге(рова(5, Х)) . вяге(5) — преаположение теоремы и ге(5) + 1 > вяге(5) — по аксиоме В 2.
Теперь мы применяем индукцию типов данных для того, чтобы доказать справедливость 5!ге(5) + ! > 5)ге(5) для генератора пеи51асХ и конструктора рпвл, тоесть нам нужнодоказать истинность Р(пеи51асг) и Р(ровп(5. я ) ). + База индукции. Заменим 5 на пенвгасХ и покажем истинность нашего предиката; 0 + 1 > 0 + Π— простой иатеиагимесний факт ввге(пеивгаск) > 1 > и ге(пеив(асв) — по аксиоие 7 Итак, для 5 = пеивгасХ теорема доказана и таким образом построена база для индукции. + Индукционныйпереход. Предположим,чтодля 5теорема выполняется, тоесть 5)ге(5) + 1 > впге(5). Покажем, что тогда она выполняется и для 5' = рцвл(5, Х): вяге(5) + 1 > вяге(5) — индукционное предположение вяге(5) + 1 + 1 > ю ге(5) + 1 — аобавии 1 н обеим насгям неравенства вяге(рыл(5.
Х)) + 1 > вяге(рова(5. Х)) — по ансионе В Итак, индукционный переход также выполняется, Вывод. Мы доказали, что вяге(рова(5, Х)) > ввге(5) выполняется для всех стеков 5. 4.4. Задачи и упражнения 177 4.3. Рекомендуемая литература Формальные модели синтаксиса, синтаксического разбора и трансляции широко использую~ся при анализе и реализации компиляторов и трансляторов 1см.
ссылки в конце главы 3). В работах Стансифера (5саттз11ег) [104] подробно обсуждается применение )ь-исчттсления и денотационной семантики при разработке языков программирования. Обзор методов формального определения семантики можно найти в работах Маркотти и др. (Магсоббу) [78]; там же вы найдете описание некоторых методов. В статье Хоара и Лаусра (1апег) [52] приведен сравнительный анализ нескольких методов определения семантики простого языка. Лукас (1лсаз) и Уолк ("ттт'а]]с) [75] описали операционный метод, называемый Лепна Пе/ттгтоп!.апдиаде, который был использован для формального определения семантики языка Р1./1. В [5] представлена большая часть формального определения семантики Ат]а; аксиоматическое определение большинства конструкций языка Рааса! дано в работе Хоара [51].
Обзор методов верификации программ вы найдете в [123] и книге Ганнона (Саттпоп), Пуртило (Рпгб!о) и Зелковица (2е][соьг1бх) [43]. Алгебраические типы данных исследовались Гуттагом (Спббай) [48]. Метод формальной спецификации Челна Пепе1ортепб МеГЬос7 ('ьтПМ) описан в книге [61], а метод Х -- в статье [103], В этой главе мы смогли коснуться лишь некоторых нз многих изящных теоретических моделей и результатов исследований в области семантики программ, универсальных языков и абстрактных машин типа машин Тьториттта. 4.4. Задачи и упражнения 1.
Пополните грамматику, приведенную в табл. 3.1, следующими НФБ-правилами: <про<раина> : <обьявпение> <списон оператороя. <обьявпение> <бес1> <обьявпение> [ <бес1> «бес1>:.= бес1аге <переиенная>: <список операторов>: =- <оператор присваивания> <список операторов> ! <оператор присваивания> Разработайте атрибутивную грамматику, для которой: + оператор присваивания определен корректно в том и только в том случае, если каждая переменная в этом операторе объявлена; + протраьтма определена корректно, если все операторы присваивания в этой программе определены корректно. 2.
Покажите, но язык, сгенерированный следующей грамматикой, является регулярным языком: 5 — т а5а[а 3. Палиндром — зто строка, которая читается в обе стороны одинаково. + Покажите, что множество палиндромов нечетной длины, составленных из символов ] а, Ь), является констекстно-свободным языком. 17В Глава 4. Моделирование свойств языка 5 7 8.
9. 10. + Покажите, что множество строк нечетной длгщы, составленных из символов 10, Ь), отличных от палиндромов, также является констекстно-свободным языком. + Почему для распознавания множества палиндромов нечетной длины требуется недетерминированный автомат с магазинной памятью, а детерминированный не годится7 Пусть имеется контекстно-свободная грамматика .= 050 ! 1з1 ) 0 ) 1 Изобразите дерево вывода для 0110110. Мы знаем, что для генерации строк типа а "Ь" требуется контекстно-свободная грамматика.
Рассмотрим следующую регулярную грамматику: 5:. - а5 ) Ь5 ) а ) Ь Утверждается, что эта грамматика также генерирует а Ь". Например, а'Ь' генерируется следующим образом: 5 ~ а5 ~ аа5 ~ ааа5 ~ аааЬ5 ~ аааЬЬ5 =~ аааЬЬЬ В данном случае мы видим, что при помощи грамматики типа 3 сгенерирован язык типа 2. Объясните зто противоречие. Модифицируйте все процедуры из листинга 3.1 так, чтобы получить постфиксную запись для арифметических выражений. Может ли регулярная грамматика распознавать определенный ниже язык для подмножества выражений7 Приведите объяснение. Объясните также основное различие между атой грамматикой и грамматикой всех возможных выражений Е-~Е+Т)Т Т-~Т*Р)Р Р->3 С помощью аксиоматического метода доказательства корректности программ: + покажите, что приведенные в тексте главы два условия окончания цикла ьл~1едействительногарантируютегозавершение(подсказка:чтопроизойдет, если оба условия истинны, а цикл не завершается?); + почему требуется, чтобы функция Т была целочислешгой? Докажите правильность следующей программы целочисленного деления: )х>Оху>0) 0 .-0 г =0 и1И1е у < г оо 0001 и г -г-у; а:-0 ° 1 епв )у» г х х = г + у х о) Что произойдет, если в листинге 4.1 окажется, что В меньше О? Для какой области значений А и 0 программа гарантированно завершается и дает правильный результат7 4,4.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
