МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ

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

образования

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

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

УТВЕРЖДАЮ

_

« _» _ 20_г.

РАБОЧАЯ ПРОГРАММА ДИСЦИПЛИНЫ

Методы трансляции и компиляции (наименование дисциплины) НАПРАВЛЕНИЕ ПОДГОТОВКИ 230100 «ИНФОРМАТИКА И

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

Квалификация (степень) выпускника Бакалавр Форма обучения очная Новосибирск Программа дисциплины «Методы трансляции и компиляции»

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

Автор (авторы) Шилов Николай Вячеславович, к.ф.-м.н.

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

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

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

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

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

2. Место дисциплины в структуре образовательной программы Дисциплина (курс) «Методы трансляции и компиляции» относится к вариативной части цикла профессиональных дисциплин ОП бакалавра.

Изучение дисциплины опирается на курсы «Математическая логика и теория алгоритмов» (теория алгоритмов, теория моделей, логика предикатов), «Логические основы программирования» (неклассические логики, метод резолюций).

Содержание дисциплины является обязательным минимум для последующих курсов: «Формальные методы программной инженерии», «Анализ алгоритмов», «Интеллектуальные системы».

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

Дисциплина формирует следующие компетенции:

ПК-26 Владеет теоретическими основами программирования, основами логического и декларативного программирования ПК-27 Владеет методами трансляции, компиляции, верификации и статического анализа программ ПК-38 Понимает роль компилятора в формировании эффективного исполнительного кода Дисциплина участвует в формировании следующих компетенций:

ОК-1 владеет культурой мышления, способен к обобщению, анализу, восприятию информации, постановке цели и выбору путей ее достижения ОК-6 стремится к саморазвитию, повышению своей квалификации и мастерства В результате освоения дисциплины студент должен:

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

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

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

Объем дисциплины и виды учебной работы – 4 зачетных единицы, единица на семестровый курс лекций, 1 единица на лабораторные работы в течение семестра, 1 единица – на самостоятельную работу. Форма аттестации – экзамен.

Содержание разделов и тем курса.

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

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

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

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

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

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

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

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

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

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

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

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

Виртуальная машина и реальная платформа. Функциональный подход к проектированию трансляторов.

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

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

Тема 5: Основы дедуктивная верификация вычислительных программ Лекция Частичная и тотальная корректность вычислительных программ.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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. Материально-техническое обеспечение дисциплины не требуется Рецензент (ы) _ Программа одобрена на заседании _ (Наименование уполномоченного органа вуза (УМК, НМС, Ученый совет) от _ года.