Министерство образования и науки Российской Федерации
Государственное образовательное учреждение высшего профессионального образования
«Новосибирский государственный университет» (НГУ)
Факультет информационных технологий
УТВЕРЖДАЮ
_______________________
« ___» _____________ 20___г.
РАБОЧАЯ ПРОГРАММА ДИСЦИПЛИНЫ
Методы трансляции и компиляции
(наименование дисциплины)
НАПРАВЛЕНИЕ ПОДГОТОВКИ 230100 «ИНФОРМАТИКА И ВЫЧИСЛИТЕЛЬНАЯ ТЕХНИКА»
Квалификация (степень) выпускника
Бакалавр
Форма обучения очная
Новосибирск
2011
Программа дисциплины «Методы трансляции и компиляции» составлена в соответствии с требованиями ФГОС ВПО к структуре и результатам освоения основных образовательных программ бакалавриата по «Профессиональному» циклу по направлению подготовки «Информатика и вычислительная техника», а также задачами, стоящими перед Новосибирским государственным университетом по реализации Программы развития НГУ.
Автор (авторы) , к. ф.-м. н.
(ФИО, ученая степень, ученое звание)
Факультет информационных технологий
Кафедра общей информатики
1. Цели освоения дисциплины (курса)
Дисциплина (курс) «Методы трансляции и компиляции» имеет своей целью: освоение студентами основ, методов и междисциплинарных связей синтаксиса, формальной семантики и трансляции языков программирования, а так же формальной спецификации, верификации и оптимизации программ.
Для достижения поставленной цели выделяются задачи курса:
1. преодолеть однобокость учебных программ, посвященных в основном синтаксическим аспектам трансляции и машинно-ориентированным аспектам оптимизации и кодогенерации;
2. уделить особое внимания современной семантике языков программирования, семантическим вопросам трансляции и формальной верификации программ.
2. Место дисциплины в структуре образовательной программы
Дисциплина (курс) «Методы трансляции и компиляции» относится к вариативной части цикла профессиональных дисциплин ОП бакалавра.
Изучение дисциплины опирается на курсы «Математическая логика и теория алгоритмов» (теория алгоритмов, теория моделей, логика предикатов), «Логические основы программирования» (неклассические логики, метод резолюций).
Содержание дисциплины является обязательным минимум для последующих курсов: «Формальные методы программной инженерии», «Анализ алгоритмов», «Интеллектуальные системы».
3. Компетенции обучающегося, формируемые в результате освоения дисциплины:
Дисциплина формирует следующие компетенции:
ПК-26 | Владеет теоретическими основами программирования, основами логического и декларативного программирования |
ПК-27 | Владеет методами трансляции, компиляции, верификации и статического анализа программ |
ПК-38 | Понимает роль компилятора в формировании эффективного исполнительного кода |
Дисциплина участвует в формировании следующих компетенций:
ОК-1 | владеет культурой мышления, способен к обобщению, анализу, восприятию информации, постановке цели и выбору путей ее достижения |
ОК-6 | стремится к саморазвитию, повышению своей квалификации и мастерства |
В результате освоения дисциплины студент должен:
иметь представление о формализмах задания синтаксиса и семантики языков программирования и спецификации программ, о процессе трансляции программ (включая лексический, синтаксический анализ и кодогенерацию), о задаче статического анализа программ и формальной верификации вычислительных и резидентных программ, о методах дедуктивной верификации вычислительных программ и методе верификации моделей для резидентных программ;
знать
l классификацию грамматик и языков по Н. Хомскому, средства задания контекстно-свободных языков синтасическими диаграммаи и в нотации Бэкуса – Наура, алгоритм синтаксического разбора контекстно-свободных языков Кока – Янгера –Касами,
l структурную операционную (по Г. Плоткину) и аксиоматичекую семантику (по А. Хоару) итеративных вычислительных программ,
l методы А. Хоара и Р. Флойда доказательства корректности итеративных вычислительных программ, метод Э. Дейкстры генерации условий корректности первого порядка для аннотированных итеративных вычислительных программ;
уметь
l строить контекстно-свободную грамматику, синтаксические диаграммы и формы Бэкуса – Наура для основных синтаксических понятий императивных языков программирования,
l производить синтаксический разбор для основных конструкций языков программирования с контекстно-свободным синтаксисом,
l специфицировать с помощью пред - и пост - условий вычислительные простые программы, аннотировать их инвариантами циклов,
l применять методы А. Хоара и Р. Флойда для доказательства «в ручную» корректности простых итеративных вычислительных программ,
l генерировать условия корректности первого порядка для полностью аннотированных простых императивных программ,
l специфицировать с помощью условий безопасности, прогресса и справедливости поведение простых императивных резидентных программ.
4. Структура и содержание дисциплины.
Структура
Объем дисциплины и виды учебной работы – 4 зачетных единицы, 1 единица на семестровый курс лекций, 1 единица на лабораторные работы в течение семестра, 1 единица – на самостоятельную работу. Форма аттестации – экзамен.
№ п/п | Раздел дисциплины | Семестр | Неделя семестра | Виды учебной работы, включая самостоятельную работу студентов и трудоемкость (в часах) | Формы текущего контроля успеваемости (по неделям семестра) Форма промежуточной аттестации (по семестрам) | |||
Лекции | Семинары | Самостоятельная работа | Экзамен | |||||
1 | Верифицирующий Компилятор – Challenge Антони Хоара | 6 | 1-2 | 4 | 0 | 0 | ||
2 | Введение в синтаксис языков программирования | 3-5 | 6 | 8 | 8 | |||
3 | Введение в семантику языков программирования | 6-8 | 6 | 8 | 8 | |||
4 | Введение в трансляцию языков программирования | 9-11 | 6 | 8 | 20 | Коллоквиум | ||
5 | Основы дедуктивная верификация вычислительных программ | 12-14 | 6 | 6 | 6 | |||
6 | Некоторые современные проблемы теории и технологии трансляции, анализа и верификации программ | 15-16 | 4 | 2 | 2 | |||
7 | Экзамен | 17 | 36 | Экзамен | ||||
ИТОГО: | 32 | 32 | 44 | 36 |
Содержание разделов и тем курса.
Семестр 6
Лекции
Тема 1: Верифицирующий Компилятор - Challenge Антони Хоара
Лекция 1
Что такое язык программирования? – Неформальное введение в Недетерминированный Модельный язык программирования НеМо. Что такое язык спецификаций? – Спецификация вычислительных программ пред - и пост-условиями и инвариантами циклов. Примеры верификации вручную вычислительных программ методом Флойда.
Тема 2: Введение в синтаксис языков программирования
Лекция 2
Язык = синтаксис + семантика + прагматика.
Язык программирования =
= формальный синтаксис + операционная семантика + область применения.
Язык спецификаций =
= формальный синтаксис + логическая семантика + область применения.
Нотация Бекуса-Наура и синтаксические диаграммы Вирта. Определение синтаксиса НеМо в формализмах Бекуса-Наура и синтаксических диаграмм.
Лекция 3
Грамматики и синтаксическая классификация Хомского. Эквивалентность формализмов Бекуса-Наура и синтаксических диаграмм контекстно-свободным грамматикам. Регулярные грамматики и конечные автоматы. Распознание регулярных языков. Сканирование лексем.
Лекция 4
Синтаксический разбор контексто –свободных языков. Алгоритм Кока – Янгера –Касами распознания и синтаксического анализа контекстно-свободных языков.
Тема 3: Введение в семантику языков программирования
Лекция 5
Семантика типов данных языка НеМо: “операционный” (теоретио-множественная) и “денотационный” (алгебраический) подходы.
Лекция 6
Традиционная и структурная операционная семантики языка НеМо и их связь(непротиворечивость и полнота).
Лекция 7
Денотационная семантика языка НеМо, её связь с традиционной и структурной операционной семантиками (непротиворечивость и полнота).
Тема 4: Введение в трансляцию языков программирования
Лекция 8
Постановка задачи трансляции. Понятие компиляции и интерпретации. Виртуальная машина и реальная платформа. Функциональный подход к проектированию трансляторов.
Лекция 9
Виртуальная машина и “виртуальная” операционная семантика языка НеМо.
Лекция 10
Трансляция НеМо: компиляция исходников и интерпретация внутреннего представления, доказательство корректности трансляции.
Тема 5: Основы дедуктивная верификация вычислительных программ
Лекция 11
Частичная и тотальная корректность вычислительных программ. Аксиоматическая семантика языка НеМо, её связь со структурной операционной семантикой (непротиворечивость).
Лекция 12
Условия корректности программ, проблема их генерации и автоматического “доказательства”. Полностью аннотированные программы, генерация и доказательство условий корректности для таких программ.
Лекция 13
Основы автоматического доказательства условий корректности. Разрешимые теории и разрешающие процедуры: двузначная логика, теория равенства, арифметика Пресбургера.
Тема 6: Некоторые современные проблемы теории и технологии трансляции, анализа и верификации программ.
Лекция 14
Верификация моделей программ методом model checking. Логика дерева вычислений: формализм для представления свойств живости и безопасности, алгоритмы верификации, примеры использования.
Лекция 15
Смешанные вычисления. Протокол, остаточная программа, детерминант. Трансформационные семантики. Проекции Футамуры. Метакомпиляция.
Семинары
Тема 2: Введение в синтаксис языков программирования
Семинар 1
Упражнения по математической логике и теории множеств (основные понятия, операции, теоремы).
Семинар 2
Упражнения по конечным автоматам, регулярным грамматикам и языкам (теоретико-множественные операции, лемма о разрастании).
Семинар 3
Упражнения по контекстно-свободным языкам (теоретико-множественные операции, лемма о разрастании, приведение к нормальной форме Хомского).
Семинар 4
Упражнения на построение дерева синтаксического разбора для контекстно-свободных языков. Практическое знакомство с нотацией Бэкуса – Наура.
Тема 3: Введение в семантику языков программирования
Семинар 5
Упражнения по абстрактным типам данных, их теоретико-множественной, алгебраической и аксиоматической семантике.
Семинар 6
Упражнения по программированию на языке НеМо. Упражнения на построение традиционной и структурной операционной семантики простых программ на языке НеМо.
Семинар 7
Упражнения на построение денотационной семантики простых программ на языке НеМо.
Семинар 8
Упражнения по спецификации программ средствами денотацтонной семантики (конструкции if-then-else и while-do).
Тема 4: Введение в трансляцию языков программирования
Семинар 9
Упражнения на составление программ для виртуальной НеМо-машины.
Семинар 10
Упражнения на построение операционной семантики простых программ на языке виртуальной НеМо-машины.
Семинар 11
Упражнения по трансляции НеМо-программ в программы виртуальной НеМо-машины.
Семинар 12
Оптимизации трансляции детерминированных НеМо-программ в детерминированные программы виртуальной НеМо-машины.
Тема 5: Основы дедуктивная верификация вычислительных программ
Семинар 13
Упражнения на доказательство частичной и тотальной корректности простых алгоритмов методом Флойда и методом потенциалов.
Семинар 14
Упражнения на доказательство частичной корректности аннотированных НеМо-программ в аксиоматической семантике языка НеМо.
Семинар 15
Упражнения на применение разрешающих процедур для доказательства истинности условий корректности.
5. Образовательные технологии
Рекомендуется еженедельно выполнять домашнее задание. В качестве подготовки к семинару прочитывать и разбирать последние лекции.
6. Оценочные средства для текущего контроля успеваемости, промежуточной аттестации по итогам освоения дисциплины и учебно-методическое обеспечение самостоятельной работы студентов
Список тем (заданий) для самостоятельной практической работы:
1. Синтаксический анализатор для языка НеМо.
2. Интерпретатор языка виртуальной НеМо-машины.
3. Транслятор вычислительных НеМо-программ в программы виртуальной НеМо-машины.
Примерный перечень вопросов к зачету (экзамену) по всему курсу.
1. Нотация Бекуса – Наура и синтаксические диаграммы Вирта. Определение синтаксиса модельного языка НеМо в формализмах Бекуса – Наура и синтаксических диаграмм.
2. Грамматики и синтаксическая классификация Хомского. Эквивалентность формализмов
Бекуса-Наура и синтаксических диаграмм контекстно-свободным грамматикам.
3. Регулярные грамматики, регулярные выражения и конечные автоматы. Распознание регулярных языков. Сканирование лексем.
4. Синтаксический разбор контекстно –свободных языков. Алгоритм Кока – Янгера – Касами распознания и синтаксического анализа контекстно-свободных языков.
5. Семантика типов данных модельного языка НеМо: «операционный» (теоретио-множественная), «аксиоматический» (по Милнера), «денотационный» (алгебраический) подходы.
6. Виртуальная машина и «виртуальная» операционная семантика модельного языка НеМо.
7. Структурная операционная семантика модельного языка НеМо, её связь с виртуальной операционной семантикой (непротиворечивость и полнота).
8. Денотационная семантика модельного языка НеМо, её связь со структурной операционной семантикой (непротиворечивость и полнота).
9. Аксиоматическая семантика модельного языка НеМо, её связь со структурной операционной семантикой (непротиворечивость и арифметическая полнота).
10. Постановка задачи трансляции. Понятие компиляции и интерпретации. Виртуальная машина и реальная платформа. Функциональный подход к проектированию трансляторов.
11. Трансляция модельного языка НеМо: компиляция исходников и интерпретация внутреннего представления.
12. Частичная и тотальная корректность вычислительных программ. Условия корректности программ, проблема их генерации и автоматического «доказательства».
13. Полностью аннотированные программы, генерация и «доказательство» условий корректности для таких программ.
14. Разрешимые теории и разрешающие процедуры: двузначная логика, теория равенства,
арифметика Пресбургера.
15. Логика дерева вычислений: формализм для представления свойств живости и безопасности. Алгоритмические проблемы для логики дерева вычислений: разрешимость, аксиоматезируемость, проверка моделей.
16. Смешанные вычисления. Протокол и остаточная программа. Трансформационные семантики.
7. Учебно-методическое и информационное обеспечение дисциплины
а) основная литература:
1. А. Ахо, Дж. Ульман. Теория синтаксического анализа, перевода и компиляции, 2 тома. М.:Мир, 1978.
2. А. Ахо, Р. Сети, Дж. Ульман. Компиляторы: принципы, технологии и инструменты. М.: Издательский дом ''Вильямc'', 2001.
3. . Смешанные вычисления. Учебное пособие. Новосибирский государственный университет, 1995.
4. Д. Грис. Конструирование компиляторов для цифровых вычислительных машин. М.: Мир, 1975.
5. Д. Грис. Наука программирования. М.:Мир, 1984.
6. Э. Кларк, О. Грамберг, Д. Пелед Верификация моделей программ. М.: МЦНМО, 2002.
7. , . Прикладные методы верификации программ. М.: Радио и связь, 1988.
б) дополнительная литература:
1. Семантика языков программирования. Сборник статей. М.: Мир, 1977.
2. M. Gordon: Programming language Theory and its Implementation. Prentice Hall, 1988.
8. Материально-техническое обеспечение дисциплины
не требуется
Рецензент (ы) _________________________
Программа одобрена на заседании ___________________________________
(Наименование уполномоченного органа вуза (УМК, НМС, Ученый совет)
от ___________ года.
