Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины)



Скачать 136.37 Kb.
Дата15.01.2013
Размер136.37 Kb.
ТипРабочая программа


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

«Новосибирский государственный университет» (НГУ)
Факультет информационных технологий

УТВЕРЖДАЮ

_______________________

« ___» _____________ 20___г.

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

Методы трансляции и компиляции

(наименование дисциплины)

НАПРАВЛЕНИЕ ПОДГОТОВКИ 230100 «ИНФОРМАТИКА И ВЫЧИСЛИТЕЛЬНАЯ ТЕХНИКА»

Квалификация (степень) выпускника

Бакалавр
Форма обучения очная

Новосибирск

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

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

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

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

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

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


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

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

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

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


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

ПК-26

Владеет теоретическими основами программирования, основами логического и декларативного программирования

ПК-27

Владеет методами трансляции, компиляции, верификации и статического анализа программ

ПК-38

Понимает роль компилятора в формировании эффективного исполнительного кода


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

ОК-1

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

ОК-6

стремится к саморазвитию, повышению своей квалификации и мастерства


В результате освоения дисциплины студент должен:

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

знать

  • классификацию грамматик и языков по Н. Хомскому, средства задания контекстно-свободных языков синтасическими диаграммаи и в нотации Бэкуса – Наура, алгоритм синтаксического разбора контекстно-свободных языков Кока – Янгера –Касами,

  • структурную операционную (по Г. Плоткину) и аксиоматичекую семантику (по А. Хоару) итеративных вычислительных программ,

  • методы А. Хоара и Р. Флойда доказательства корректности итеративных вычислительных программ, метод Э. Дейкстры генерации условий корректности первого порядка для аннотированных итеративных вычислительных программ;

уметь

  • строить контекстно-свободную грамматику, синтаксические диаграммы и формы Бэкуса – Наура для основных синтаксических понятий императивных языков программирования,

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

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

  • применять методы А. Хоара и Р. Флойда для доказательства «в ручную» корректности простых итеративных вычислительных программ,

  • генерировать условия корректности первого порядка для полностью аннотированных простых императивных программ,

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

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. Материально-техническое обеспечение дисциплины

не требуется
Рецензент (ы) _________________________
Программа одобрена на заседании ___________________________________

(Наименование уполномоченного органа вуза (УМК, НМС, Ученый совет)

от ___________ года.



Похожие:

Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины) iconПрограмма дисциплины «Теория языков программирования и методы трансляции»

Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины) iconРабочая программа дисциплины Теория автоматического управления (Наименование дисциплины) Направление подготовки

Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины) iconРабочая программа дисциплины теория и устройство судна (Наименование дисциплины) Направление подготовки

Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины) iconРабочая программа дисциплины Основы теории управления (Наименование дисциплины) Направление подготовки

Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины) iconРабочая программа дисциплины химия полное наименование дисциплины для специальности (ей)/ направления подготовки

Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины) iconРабочая программа дисциплины «Механика» полное наименование дисциплины

Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины) iconРабочая программа учебной дисциплины «Физико-химические методы исследования и техника лабораторных работ»
Рабочая программа учебной дисциплины может быть использована для переподготовки средних медицинских работников по разделам: «Физико-химические...
Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины) iconРабочая программа Дисциплины «Теория принятия решений» (наименование дисциплины) для специальности(ей) 080801 «Прикладная информатика (в юриспруденции)» (номер и наименование специальности)
Государственного образовательного стандарта высшего профессионального образования, утвержденного 14. 03. 2000 г
Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины) iconРабочая программа преподавания дисциплины «Информационные технологии в экономике» наименование дисциплины
«Экономика и управление на предприятии (по отраслям)», утвержденного Министерством образования РФ «17» марта 2000 г.; государственная...
Рабочая программа дисциплины методы трансляции и компиляции (наименование дисциплины) iconПрограмма наименование дисциплины агрохимические методы исследований
...
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org