Formal Syntax And Semantics of Programming Language

Почитал книгу Addison Wesley Formal Syntax And Semantics of Programming Language 1995 654 стр.

Давно хотел разобраться с формальными методами спецификации языков и проверки правильности программ, а в данной книге охвачено большое их количество. Книга является учебником по курсу формальных методов и настоятельно рекомендует практические занятия (лабораторные) на Прологе.

Глава 1. Спецификация синтаксиса

Все мы помним, что синтаксис это форма записи, а семантика это смысл в этих формах.

В этой главе: БНФ, контекстно зависимые и контекстно-свободные граматики, регулярные выражения.

Абстрактный/конкретный синтаксис. Если взять синтаксис языка, можно найти множество лексем служащих для облегчения однозначности построения дерева разбора. Например, скобки для обозначения приоритета "(2+5)*3" или ";" между отдельными инструкциями в списке инструкций. После получения дерева разбора, эти элементы больше не нужны и их можно более не рассматривать. Оставшиеся элементы существенны для дальнейшего анализа. Они и составляют абстрактный синтаксис.

Глава 2. Введение в практические занятия

Сканер на Прологе. Техника "логических грамматик" (Logic Grammars). Парсер на Прологе. Такие себе прологовые извращения.

Глава 3. Атрибутные грамматики

Понятие атрибутных грамматик. На каждый нетерминал навешиваем множество атрибутов и правиля их вычисления по атрибутам родительского либо дочерних элементов. В первом случае это наследуемые атрибуты, во втором - синтезируемые.

Атрибутные граматики можно использовать для проверки контекстных условий и для спецификации семантики (например, семантика десятичных чисел "[0-9]+" определяется как значение этих чисел, сами значения вычисляются при помощи атрибутной грамматики).

Глава 4. Двухуровневые грамматики

Применяются для проверки контекстных условий. Не читал.

Глава 5. Лямбда исчисление

• Способно выразить все исчисляемые функции
• Играет важную роль для функциональных языков, напрямую отражает их суть.
• Является базой для денатационной семантики (denotational semantic)

Все объекты представлены функциями (от одной переменной), (даже натуральные числа). Функция получает другую функциюи как аргумент и возвращает функцию как результат.

Семантика лямбда исчеслений выражается через правила подстановки аргумента и упрощения выражений.

Глава 6. Самоопределение языков программирования

Лисп на Лиспе и Пролог на Прологе. Красиво, кратко. Не то что Ада на Аде :( Хотя практическая ценность сомнительна.

Глава 7. Трансляционная семантика

Придумывается целевая машина и семантика языка задается как правила трансляции конструкций языка в ассемблер этой машины (используя атрибутную грамматику). Типичный пример реализации компилятора. Все просто и никому не нужно :)

Глава 8. Традиционная операционная семантика (Operational Semantic)

Операционная семантика определяет как выполняются вычисления в программе (а не что вычисляет программа, как в некоторых других семантиках). При помощи определения состояния или "конфигурации" задается абстракная машина и как конструкции языка изменяют состояния машины. Пример состояния: набор ячеек для хранения значений переменных (как отношение адрес-номер-ячейки -> целое-или-логическое-значение), отражение имен идентификаторов на адреса ячеек, для определения семантики деклараций переменных (как отношение имя -> адрес-номер-ячейки). VDL пример такой семантики. Этот метод дает сложные для построения и понимания спецификации, с кучей (излишних?) подробностей.

Машина SECD для исполнения лямбда исчеслений.

Структурная операционная семантика. Основал Плоткин. Красивая спецификация в которой роль исполняющей машины выполняет машина логического вывода. Основная конструкция:

П1 П2 ... Пn
------------ У(словие)
 З(аключение)

где П1 - посылка1 и т.д.

Хитрый метод спецификации абстрактного синтаксиса, когда П1 .. Пn - дочерние элементы конструкции З. К нему же метод структурной индукции, когда некое утверждение верно для П1 .. Пn, то оно верно для З.

Дальше идет пример семантики выражений и команд.

Структурная операционная семантика называется семантикой маленьких шагов, поскольку описывает наименьшие изменения состояния абстрактной машины. Семантика больших шагов описывает отношения между начальным и конечным состояние минуя промежуточные. Пример - натуральная семантика (Natural Semantic). В книге не рассмотрена, поскольку напоминает денотационную.

Глава 9. Денотационная семантика (Denotational Semantic)

Семантика программ задается в терминах математических понятий (множества, функции, целые числа, наборы значений).

Опять состояния и семантика команды как функция изменения состояния.

Проверка контекстных условий с помощью денотационной семантики.

Использование "продолжений" (continuation) для спецификации goto, exit, exceptions.

Основана на теории (рекурсивных) функций и лямбда исчислении.

Глава 10. Теория доменов и "фиксированной точки"

Че-то касающееся доказательства корректности использования рекурсии и вопросов незавершения вычислений. Символ bottom (вот откуда он в TenDRA) для обозначения незавершения.

Ниасилил.

Глава 11. Аксиоматическая семантика (Axiomatic Semantic)

До боли знакомая модель. Наверное по другим книжкам (типа ANNA для Ады). Механизм состояния не используется. Вместо этого - набор отношений (между значениями переменных) пре и пост-условия. Две программы эквивалентны если при выполненых преусловиях делают пост-условия. Особенности архитиктуры (размеры слов) не учитываются. Основана Флойдом и Хоаром. Имеет ряд ограничений: запрещается сторонние эфекты в выражениях, трудно с goto, нельзя иметь синонимы (aliasing) и перегрузку (overloading) идентификаторов. Используется для доказательства коррекстности программ.

Основана на теории предикатов.

Глава 12. Алгебраическая семантика (Algebraic Semantic)

Основана на абстрактной алгебре. Sort-ы (сорт, род, тип, вид - сорт наверное правильнее всего, т.к. мультисортная алгебра) и операции над ними зщадают сигнатуру алгебры и (абстрактный) синтаксис. Семантика задается уравнениями, аксиомами.

Модульность описаний с возможностью настраиваемых (generic) модулей.

Дальше непереводимый математический жаргон.

Используется (в том числе) для описаний абстрактных типов данных (ADT), абстрактного синтаксиса (в TenDRA и конкретного тоже) ну и собственно для определения семантики.

Для алгебраической семантики нарыл "стандартный" язык и тулзы на Джаве http://www.informatik.uni-bremen.de/cofi/wiki/index.php/CASL

Глава 13. Cемантика действий(?) (Action Semantic)

Питер Мозес (Peter Mosses) придумал чтобы облегчить практическое применение формальных методов. Прямо отражает обычные концепции языков программирования. Имеет формальную спецификацию. Развита из денотационной, но не содержит функций высокого порядка (действия не оперуруют действиями). Три типа (facets) "ортогоналтных" обозначений: actions, data и yealders. Синтаксис близкий к английскому.

Это как бы метаязык, каждая фраза которого имеет формальное определение. Может быть использован, как, своего рода, язык промежуточного представления (IR). Тогда формальная спецификация языка задает схему преобразования из языка в action semantic, затем результат преобразование интерпретируется или компилируется. Как нечто имеющее формальную спецификацию Action Semantic может быть использован при проверке фаз трансляции.

Мосес использовал подмножество Ады для илюстраций в своих работах по Action Semantic. Упоминается формальная спецификация ANDF (aka TDF), но достать врядли выйдет.

Такое вот привлекательное со всех сторон, останавливает только то, что оно как-то подозрительно затихло. На сайте нет новостей и список рассылки давно устарел http://www.brics.dk/Projects/AS/index.html