Часть II. Формальное описание языков программирования ( Формальная спецификация формальных языков ) Введение. Атрибутные грамматики

План 1.Цели и задачи формального описания языков программирования 2.Синтаксис, семантика, прагматика (статическая и динамическая семантики) 3.Подходы к описанию (контекстно-свободного) синтаксиса 4.Подходы к описанию контекстно-зависимого синтаксиса (статической семантики) 5.Подходы к описанию (динамической) семантики

Цели 1.Автоматическая генерация программ 2.Автоматическая верификация 3.Недвусмысленное (строгое) описание языка 4.Апробация новых концепций при разработке новых языков

Задачи формального описания Описание контекстных зависимостей (статической семантики) 1.Описать требования к (статически) корректной программе (для пользователя языка, для разработчика тестов компилятора, для разработчика компилятора) 2.Сформировать исходные данные для генератора фронт-процессора Описание «смысла», динамической семантики 1.Описать эталон, с которым можно сравнивать результаты выполнения скомпилированной программы 2.Сформировать исходные данные для генератора кода компилятора 3.Описать правила (аксиомы) эквивалентности, которые можно использовать для построения оптимизаторов 4.Описать правила (аксиомы) эквивалентности, которые можно использовать для верификации оптимизаторов Спецификация блоков компилятора и компилятора в целом 1.Сформировать исходные данные для построения тестов для компилятора в целом и для отдельных блока компилятора

Сесантический свойства (аспекты) языка 1.Передача параметров 2.Порядок вычислений параметров функций 3.Области видимости имен 4.Размещение данных в памяти 5.Обработка исключений, более широко, поведение при ненормальном ходе вычислений 6.Синхронизация и взаимодействие параллельных ветвей (нитей) программы 7.Динамическое связывание программ 8.Сбор мусора

Другие приложения формальных описаний языков 1.Разработка и тестирование протокольных сообщений (язык построения заголовков) 2.Генерация html документов, тестирование процессоров html документов, например, браузеров. 3.Генерация XML документов, тестирование процессоров XML документов 4.Какие еще области используют формальные языки?

Синтаксис, семантика (статическая и динамическая), прагматика Синтаксис - структура, Семантика –статическая - корректность –динамическая - смысл, Прагматика – назначение

Язык и грамматика Язык 1 – множество предложений. Грамматика – множество правил, которые описывают порождение предложений языка. Язык 2 – множество предложений, которые порождаются из данной грамматики. Синтаксис – описание структуры предложений. Структура – набор элементов и связей между ними. Каждому слову сопоставляется его (грамматическая) роль и задаются связи между словами, между группами слов (фразами). Контекстно-свободные грамматики, контекстно-свободный синтаксис. Контекстно-зависимый синтаксис (context-sensitive, статическая семантика)

Грамматика Алфавит: конечный набор символов Σ Строки: конечные цепочки символов Пустая строка ε Σ* - множество всех возможных строк из символов Σ (включая ε) Σ+ - множество всех непустых строк из символов Σ Язык: множество строк L Σ*

Грамматики G = (N, T, S, P) Конечное множество нетерминальных символов N Конечное множество терминальных символов T Стартовый нетерминальный символ S N Конечное множество продукций P Продукция: x y x (N T) +, y (N T)* Применение продукции: uxv ayb

Языки и грамматики Вывод строки w 1 w 2 … w n ; обозначается как w 1 w n Язык, которые генерируется грамматикой L(G) = { w T* | S w } Традиционная классификация –Регулярные (Regular) –Контекстно-свободные (Context-free) –Контекстно-зависимые (Context-sensitive) –Все остальные (Unrestricted)

Контекстно-свободные (КС) языки Выход за границы регулярных языков –L = { a n b n | n > 0 } КС, но не регулярный Генерируется КС грамматикой Все продукции имеют вид: A w, где –A N, w (N T)* BNF: –Backus-Naur form: John Backus and PeterNaur, for ALGOL60

Пример расширенной BNF (EBNF) ::= while do | if then [ else ] | := | ( {, } ) Введены сокращения: [ … ] - цепочка, которая может быть опущена { … } - цепочка, которая может отсутствовать или повторяться некоторое число раз

Дерево вывода Другие названия: дерево разбора (parse tree) или дерево конкретного синтаксиса (concrete syntax tree) –Листья - терминалы –Внутренние узлы - нетерминалы –Корень – стартовый нетерминал грамматики Описывает конкретный путь вывода заданной строки –Узлы-листья слева направо составляют заданную входную цепочку обход графа «сначала вглубь», начиная с самой левой непройденной вершины

Пример дерева вывода

Ограничения КС грамматик Не могут представлять семантику, например –«каждая переменная должна быть описана ранее, чем ее используется» –«использование переменной должно быть согласовано с ее типом» –не описывает действия, которые скрываются за тексом, например «строка» s1 делится на «строку» s2 Решение: атрибутные грамматики –Определенный вид описания семантики

Атрибутные грамматики КС грамматика (BNF) Конечное множество атрибутов –Для каждого атрибута – область возможных значений –Для каждого терминала и нетерминала – можесвто ассоциированных с ним атрибутов (возможно, пустое) Наследуемые (inherited) и синтезируемые (synthesized) Множество правил вычисления атрибутов Множество булевских условий, заданных на значениях атрибутов

Пример L = { a n b n c n | n > 0 } – не КС BNF ::= ::= a | a ::= b | b ::= c | c Атрибуты –Na: ассоциирован с –Nb: ассоциирован с –Nc: ассоциирован с –Область значений = integers

Пример Правила вычисления (аналогично для, ) ::= a Na( ) := 1 | a 2 Na( ) := 1 + Na( 2) Условия ::= Cond: Na( ) = Nb( ) = Nc( ) Альтернативная нотация -.Na

Дерево разбора

Дерево разбора для некоторой атрибутной грамматики Корректное дерево для опорной (underlying) BNF Каждый узел имеет свой набор пар (атрибут-значение) Некоторые узлы имеют булевские условия Корректное дерево разбора –Значения атрибутов отвечают правилам их вычисления –Все булевские атрибуты (условия) истинны

Пример – блок в языке Ada x: begin a := 1; b := 2; end x; ::= 1 : begin end 2 ; –Cond: value( 1) = value( 2) ::= | ::= id –value( ) := id

Другой способ задания условий.OK := 1.value = 2.value Все узлы типа должны иметь.OK = true

Синтезируемые vs. наследуемые атрибуты Синтезируемые атрибуты вычисляются, используя значения из деревьев-потомков –Продукция - ::= … –Правило вычисления -.syn := … Наследуемые – значения из узла-родителя –Продукция - ::= … … –Правило вычисления -.inh := … В обоих случаях правила вычисления могут иметь произвольную сложность

Синтезируемые и наследуемые атрибуты syn inh

Правила вычислений Синтезируемые атрибуты ассоциированные с N: –каждая альтернатива в продукции для N должна иметь правило для вычисления такого атрибута Наследуемые атрибуты ассоциированные с N: –для каждого вхождения N в правой части любой альтернативы должно быть правило для вычисления этого атрибута

Пример: двоичные числа КС грамматика Для простоты будем писать X вместо B ::= D B ::= D B D ::= 0 D ::= 1 Цель – вычислить значение двоичного числа

Пример: двоичные числа (2) B ::= D B.pos := 1 B.val := D.val D.pow := 0 B1 ::= D B2 B1.pos := B2.pos + 1 B1.val := B2.val + D.val D.pow := B2.pos D ::= 0 val := 0 D ::= 1 D.val := 2 D.pow (возведение в степень) ADD attributes B: syn val B: syn pos D: inh pow D: syn val

Дерево разбора с вычисленными атрибутами

КС грамматика ::= ::= begin ; end ::= | ; ::= | |...

Задачи Проверить типы переменных (int, bool) Для вложенных блоков использовать самые внутренние декларации (static scoping) Проверять типы параметров и тип возвращаемого значения в функциях –Например, все функции имеют тип результата int

Дерево разбора prog | block ДекларацииОператоры

Структура данных Использовать стек групп пар вида имя- тип –стек «таблиц символов» Строить таблицы символов для деклараций в блоках –синтезируемый атрибут tbl Использовать стек таблиц символов в операторах и выражениях –наследуемый атрибут symtab

Пример – проверка типов begin bool i; int j; begin int i; x := i + j; end Верхушка стека [ {("i",INT)}, {("i",BOOL), ("j",INT)} ] База стека

Атрибутная грамматика ::=.symtab := emptystack ::= begin ; end.symtab := push(.tbl,.symtab) 1 ::=.symtab := 1.symtab | ; 2.symtab := 1.symtab 2.symtab := 1.symtab

Декларации 1 ::= 1.tbl :=.tbl | ; 2 1.tbl :=.tbl 2.tbl Условие: ids(.tbl) ids( 2.tbl) = ids – функция, которая получает множество вида имя-тип и возвращает множество всех имен

Декларации ::= int.tbl := { (.name, INT) } | bool.tbl := { (.name, BOOL) } | fun ( ) : int =.tbl := { (.name, FUN(.types, INT) ) }.symtab := Oops!……. Синтезируемый атрибут - упорядоченный список INT/BOOL

Возврат к.symtab Декларации добавляются в наследуемый атрибут symtab ::= begin ; end.symtab := push(.tbl,.symtab).symtab := push(.tbl,.symtab) Сначала берем декларации в, потом используем их для проверок блоков встроенных в

Декларации 1 ::= 1.tbl :=.tbl | ; 2 1.tbl :=.tbl 2.tbl.symtab := 1.symtab 2.symtab := 1.symtab Cond: ids(.tbl) ids( 2.tbl) =

Декларации ::= int.tbl := { (.name, INT) } | bool.tbl := { (.name, BOOL) } | fun ( ) : int =.tbl := { (.name, FUN(.types, INT) ) }.symtab := push(.tbl,.symtab)

Проверка типов в теле функции fun f (int i): int = begin... g(5)... end; fun g (int j): int = begin... end

Операторы 1 ::=.symtab := 1.symtab | ;.symtab := 1.symtab 2.symtab := 1.symtab ::=.symtab :=.symtab |.symtab :=.symtab | if then else....symtab :=.symtab

Операторы ::= :=.symtab :=.symtab typeof(.name,.symtab) = INT | :=.symtab :=.symtab typeof(.name,.symtab) = BOOL

Выражения 1 ::= Cond: typeof(.name, 1.symtab) = INT | symtab := 1.symtab 3.symtab := 1.symtab | false Cond: typeof(.name,.symtab) = BOOL

Вызов функции (Function Call) ::= ( ) Cond: typeof(.name,.symtab) = FUN Cond: rettype(.name,.symtab) = INT.expTypes := paramtypes(.name,.symtab).symtab :=.symtab

Резюме по атрибутным грамматикам (1) АГ хороши для спецификации контекстно- свободных языков Техника построена комбинации вычислений синтезируемых и наследуемых атрибутов Последовательность вычислений атрибутов может определяться автоматически Имеется возможности для для отсеивания некорректных деревьев разбора

Резюме по атрибутным грамматикам (2) Глобальные структуры данных (окружение ) передается через атрибуты Глобальные счетчики (например, метки) реализуются как пары атрибутов Абстрактные типы данных (например, множества) используются до тех пор, пока не начинается собственно программирование Правила могут использовать вспомогательные функции Реальные применения: для проверки типов (type checking) и генерации кода (code generation)

Литература 1. Formal specification of programming languages, F.Pagan 2. Formal syntax and semantics of programming languages, Kurtz and Slonnegar.