Федеральное агентство по образованию

Государственное образовательное учреждение высшего профессионального образования

«Новосибирский государственный университет» (НГУ)

Факультет информационных технологий

Кафедра общей информатики

ПРОГРАММА

ДИСЦИПЛИНЫ МЕТОДЫ ТРАНСЛЯЦИИ И КОМПИЛЯЦИИ

ЦИКЛ* ОПД — Общепрофессиональные дисциплины НАПРАВЛЕНИЕ ПОДГОТОВКИ БАКАЛАВРОВ 230100.62 «ИНФОРМАТИКА И

ВЫЧИСЛИТЕЛЬНАЯ ТЕХНИКА»

(ФИО, ученая степень, ученое звание) Новосибирск 2009 * Наименование цикла дисциплин в соответствии с ГОС ВПО Программа дисциплины «Методы трансляции и компиляции» составлена в соответствии с требованиями к обязательному минимуму содержания и уровню подготовки бакалавра по циклу «общепрофессиональных дисциплин» Федеральных государственных образовательных стандартов высшего профессионального образования по направлению 230100.62 «Информатика и вычислительная техника».

1. Цели и задачи дисциплины (курса) Дисциплина (курс) «Методы трансляции, семантики и верификации программ» имеет своей целью: освоение студентами основ, методов и междисциплинарных связей синтаксиса, формальной семантики и трансляции языков программирования, а так же формальной спецификации, верификации и оптимизации программ.

Для достижения поставленной цели выделяются задачи курса:

1. преодолеть однобокость учебных программ, посвященных в основном синтаксическим аспектам трансляции и машинно-ориентированным аспектам оптимизации и кодогенерации;

2. уделить особое внимания современной семантике языков программирования, семантическим вопросам трансляции и формальной верификации программ.

2. Требования к уровню освоения содержания дисциплины В результате освоения дисциплины студент должен:

иметь представление о формализмах задания синтаксиса и семантики языков программирования и спецификации программ, о процессе трансляции программ (включая лексический, синтаксический анализ и кодогенерацию), о задаче статического анализа программ и формальной верификации вычислительных и резидентных программ, о методах дедуктивной верификации вычислительных программ и методе верификации моделей для резидентных программ;

знать классификацию грамматик и языков по Н. Хомскому, средства задания контекстно-свободных языков синтасическими диаграммаи и в нотации Бэкуса – Наура, алгоритм синтаксического разбора контекстно-свободных языков Кока – Янгера –Касами, структурную операционную (по Г. Плоткину) и аксиоматичекую семантику (по А. Хоару) итеративных вычислительных программ, методы А. Хоара и Р. Флойда доказательства корректности итеративных вычислительных программ, метод Э. Дейкстры генерации условий корректности первого порядка для аннотированных итеративных вычислительных программ;

уметь строить контекстно-свободную грамматику, синтаксические диаграммы и формы Бэкуса – Наура для основных синтаксических понятий императивных языков программирования, производить синтаксический разбор для основных конструкций языков программирования с контекстно-свободным синтаксисом, специфицировать с помощью пред- и пост- условий вычислительные простые программы, аннотировать их инвариантами циклов, применять методы А. Хоара и Р. Флойда для доказательства «в ручную»

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

3. Объем дисциплины и виды учебной работы Вид учебной работы Семестр Общая трудоемкость дисциплины Аудиторные занятия, в том числе: Лекции 4. Содержание дисциплины 4.1 Новизна курса (научная, содержательная; сравнительный анализ с подобными курсами в России и за рубежом).

Курс позволяет преодолеть однобокость учебной литературы на русском языке, посвящённой в основном синтаксическим аспектам трансляции языков программирования и машинно-ориентированным аспектам оптимизации и кодогенерации, но не уделяющей внимания современной семантике языков программирования, семантическим вопросам трансляции и формальной верификации программ. Особенностью курса является построение его вокруг модельного языка недетерминированного программирования НеМо. Такой подход позволяет рассказать доступно и точно о главном в трансляции, статическом анализе и верификации программ, а не отвлекаться на особенности того или иного конкретного реального языка программирования, той или иной реальной вычислительной машины. Другое достоинство такого подхода состоит в том, что для модельного языка действительно возможно на модельном уровне решить проблему верификации программ (т. е. математического доказательства хорошо специфицированных их свойств).

4.2 Тематический план курса (распределение часов по видам учебной работы).

Challenge Антони программирования программирования трансляцию языков программирования вычислительных трансляции, анализа 4.3 Содержание разделов и тем курса.

Семестр Лекции Тема 1: Верифицирующий Компилятор - Challenge Антони Хоара Лекция Что такое язык программирования? – Неформальное введение в Недетерминированный Модельный язык программирования НеМо. Что такое язык спецификаций? – Спецификация вычислительных программ пред- и пост-условиями и инвариантами циклов. Примеры верификации вручную вычислительных программ методом Флойда.

Тема 2: Введение в синтаксис языков программирования Лекция Язык = синтаксис + семантика + прагматика.

Язык программирования = = формальный синтаксис + операционная семантика + область применения.

Язык спецификаций = = формальный синтаксис + логическая семантика + область применения.

Нотация Бекуса-Наура и синтаксические диаграммы Вирта. Определение синтаксиса НеМо в формализмах Бекуса-Наура и синтаксических диаграмм.

Лекция Грамматики и синтаксическая классификация Хомского. Эквивалентность формализмов Бекуса-Наура и синтаксических диаграмм контекстно-свободным грамматикам.

Регулярные грамматики и конечные автоматы. Распознание регулярных языков.

Сканирование лексем.

Лекция Синтаксический разбор контексто –свободных языков. Алгоритм Кока – Янгера –Касами распознания и синтаксического анализа контекстно-свободных языков.

Тема 3: Введение в семантику языков программирования Лекция Семантика типов данных языка НеМо: “операционный” (теоретио-множественная) и “денотационный” (алгебраический) подходы.

Лекция Традиционная и структурная операционная семантики языка НеМо и их связь(непротиворечивость и полнота).

Лекция Денотационная семантика языка НеМо, её связь с традиционной и структурной операционной семантиками (непротиворечивость и полнота).

Тема 4: Введение в трансляцию языков программирования Лекция Постановка задачи трансляции. Понятие компиляции и интерпретации. Виртуальная машина и реальная платформа. Функциональный подход к проектированию трансляторов.

Лекция Виртуальная машина и “виртуальная” операционная семантика языка НеМо.

Лекция Трансляция НеМо: компиляция исходников и интерпретация внутреннего представления, доказательство корректности трансляции.

Тема 5: Основы дедуктивная верификация вычислительных программ Лекция Частичная и тотальная корректность вычислительных программ. Аксиоматическая семантика языка НеМо, её связь со структурной операционной семантикой (непротиворечивость).

Лекция Условия корректности программ, проблема их генерации и автоматического “доказательства”. Полностью аннотированные программы, генерация и доказательство условий корректности для таких программ.

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

Тема 6: Некоторые современные проблемы теории и технологии трансляции, анализа и верификации программ.

Лекция Верификация моделей программ методом model checking. Логика дерева вычислений:

формализм для представления свойств живости и безопасности, алгоритмы верификации, примеры использования.

Лекция Смешанные вычисления. Протокол, остаточная программа, детерминант.

Трансформационные семантики. Проекции Футамуры. Метакомпиляция.

Семинары Тема 2: Введение в синтаксис языков программирования Семинар Упражнения по математической логике и теории множеств (основные понятия, операции, теоремы).

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

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

Семинар Упражнения на построение дерева синтаксического разбора для контекстно-свободных языков. Практическое знакомство с нотацией Бэкуса – Наура.

Тема 3: Введение в семантику языков программирования Семинар Упражнения по абстрактным типам данных, их теоретико-множественной, алгебраической и аксиоматической семантике.

Семинар Упражнения по программированию на языке НеМо. Упражнения на построение традиционной и структурной операционной семантики простых программ на языке НеМо.

Семинар Упражнения на построение денотационной семантики простых программ на языке НеМо.

Семинар Упражнения по спецификации программ средствами денотацтонной семантики (конструкции if-then-else и while-do).

Тема 4: Введение в трансляцию языков программирования Семинар Упражнения на составление программ для виртуальной НеМо-машины.

Семинар Упражнения на построение операционной семантики простых программ на языке виртуальной НеМо-машины.

Семинар Упражнения по трансляции НеМо-программ в программы виртуальной НеМо-машины.

Семинар Оптимизации трансляции детерминированных НеМо-программ в детерминированные программы виртуальной НеМо-машины.

Тема 5: Основы дедуктивная верификация вычислительных программ Семинар Упражнения на доказательство частичной и тотальной корректности простых алгоритмов методом Флойда и методом потенциалов.

Семинар Упражнения на доказательство частичной корректности аннотированных НеМо-программ в аксиоматической семантике языка НеМо.

Семинар Упражнения на применение разрешающих процедур для доказательства истинности условий корректности.

4.4 Перечень примерных контрольных вопросов и заданий для самостоятельной работы.

Список тем (заданий) для самостоятельной практической работы:

1. Синтаксический анализатор для языка НеМо.

2. Интерпретатор языка виртуальной НеМо-машины.

3. Транслятор вычислительных НеМо-программ в программы виртуальной НеМомашины.

4.5 Примерная тематика рефератов, курсовых работ.

Рефератов и курсовых работ не предусмотрено.

5. Учебно-методическое и информационное обеспечение дисциплины (курса) 5.1 Примерный перечень вопросов к зачету (экзамену) по всему курсу.

1. Нотация Бекуса – Наура и синтаксические диаграммы Вирта. Определение синтаксиса модельного языка НеМо в формализмах Бекуса – Наура и синтаксических диаграмм.

2. Грамматики и синтаксическая классификация Хомского. Эквивалентность Бекуса-Наура и синтаксических диаграмм контекстно-свободным грамматикам.

3. Регулярные грамматики, регулярные выражения и конечные автоматы. Распознание регулярных языков. Сканирование лексем.

4. Синтаксический разбор контекстно –свободных языков. Алгоритм Кока – Янгера – Касами распознания и синтаксического анализа контекстно-свободных языков.

5. Семантика типов данных модельного языка НеМо: «операционный» (теоретиомножественная), «аксиоматический» (по Милнера), «денотационный»

(алгебраический) подходы.

6. Виртуальная машина и «виртуальная» операционная семантика модельного языка 7. Структурная операционная семантика модельного языка НеМо, её связь с виртуальной операционной семантикой (непротиворечивость и полнота).

8. Денотационная семантика модельного языка НеМо, её связь со структурной операционной семантикой (непротиворечивость и полнота).

9. Аксиоматическая семантика модельного языка НеМо, её связь со структурной операционной семантикой (непротиворечивость и арифметическая полнота).

10. Постановка задачи трансляции. Понятие компиляции и интерпретации. Виртуальная машина и реальная платформа. Функциональный подход к проектированию 11. Трансляция модельного языка НеМо: компиляция исходников и интерпретация внутреннего представления.

12. Частичная и тотальная корректность вычислительных программ. Условия корректности программ, проблема их генерации и автоматического «доказательства».

13. Полностью аннотированные программы, генерация и «доказательство» условий корректности для таких программ.

14. Разрешимые теории и разрешающие процедуры: двузначная логика, теория арифметика Пресбургера.

15. Логика дерева вычислений: формализм для представления свойств живости и безопасности. Алгоритмические проблемы для логики дерева вычислений:

разрешимость, аксиоматезируемость, проверка моделей.

16. Смешанные вычисления. Протокол и остаточная программа. Трансформационные 5.2 Основная литература* 1. А. Ахо, Дж. Ульман. Теория синтаксического анализа, перевода и компиляции, тома. М.:Мир, 1978.

2. А. Ахо, Р. Сети, Дж. Ульман. Компиляторы: принципы, технологии и инструменты.

М.: Издательский дом ''Вильямc'', 2001.

3. М.А. Бульонков. Смешанные вычисления. Учебное пособие. Новосибирский государственный университет, 1995.

4. Д. Грис. Конструирование компиляторов для цифровых вычислительных машин. М.:

5. Д. Грис. Наука программирования. М.:Мир, 1984.

6. Э. Кларк, О. Грамберг, Д. Пелед Верификация моделей программ. М.: МЦНМО, 2002.

Не более 10 источников.

7. В.А. Непомнящий, О.М. Рякин. Прикладные методы верификации программ. М.:

Радио и связь, 1988.

5.3 Дополнительная литература.

1. Семантика языков программирования. Сборник статей. М.: Мир, 1977.

2. M. Gordon: Programming language Theory and its Implementation. Prentice Hall, 1988.

5.4 Программное и коммуникационное обеспечение не требуется.

6. Методические рекомендации по организации изучения дисциплины Рекомендуется еженедельно выполнять домашнее задание. В качестве подготовки к семинару прочитывать и разбирать последние лекции.