Кафедра общей информатики ФИТ НГУ

Программа курса «Основы трансляции,

статического анализа и верификации программ»

2003-2004 учебный год

1. Организационно-методический раздел.

1.1 Название курса.

Основы трансляции, статического анализа и верификации программ Направление - 552800 Информатика и вычислительная техника.

Раздел - специальные дисциплины Компонент - СД.0? вузовский 1.2 Цели и задачи курса.

1.3 Требования к уровню освоения содержания курса.

1.4 Формы контроля Итоговый контроль. Для контроля усвоения дисциплины учебным планом предусмотрены:

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

2 Содержание дисциплины.

2.1 Новизна.

2.2 Тематический план курса.

5 семестр Количество часов Наименование разделов и тем Лаборатор- Самостоятель- Всего Лекции Семинары ные работы ная работа часов Верифицирующий Компилятор 8 4 - Challenge Антони Хоара Введение в синтаксис языков 8 4 программирования Введение в семантику языков 10 5 программирования Введение в трансляцию языков 4 2 программирования Основы статического анализа и 8 4 оптимизации программ Основы дедуктивная 6 3 верификация вычислительных программ Основы автоматическая 6 3 верификация резидентных программ Некоторые современные 10 5 проблемы теории и технологии трансляции, анализа и верификации программ Практикум - 6 2 Итого по курсу: 60 6 0 32 Кафедра общей информатики ФИТ НГУ Программа курса «Основы трансляции, статического анализа и верификации программ»

2003-2004 учебный год 2.3 Содержание отдельных разделов и тем.

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

- Лекция Примеры верификации вручную вычислительных программ методом Флойда. Примеры верификации вручную резидентных программ с использованием проблемно-ориентированных принципов МанныПнуэли.

- Лекция Язык = синтаксис + семантика + прагматика.

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

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

- Лекция Воспоминания о математической логике: синтаксис, семантика и прагматика пропозициональной логики, исчисления предикатов первого и высших порядков; неклассические логики; теории и методы их задания;

разрешающие и полуразрешающие процедуры.

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

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

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

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

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

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

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

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

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

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

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

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

• Основы статического анализа и оптимизации программ - Лекция Машинно-независимая оптимизация программ: вычисления над константами, удаление общих подвыражений, оптимизация логических выражений и вынесение инвариантных вычислений за цикл.

Генерация кода и машинно-зависимая оптимизация.

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

- Лекция Основы теории абстрактной интерпретации: монотонные отображения частично-упорядоченных множеств, теорема Тарского-Кнастера о неподвижных точках, связки Галуа.

- Лекция Примеры анализа НеМо программ с использованием абстрактной интерпретации: просачивание констант, анализ интервалов, конгруэнтный анализ.

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

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

- Лекция Аксиоматизируемые теории и полуразрешающие процедуры. Метод резолюций.

• Основы автоматическая верификация резидентных программ - Лекция Логика дерева вычислений: формализм для представления свойств живости и безопасности.

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

- Лекция Абстракция и проверка конечных моделей для логики дерева вычислений. Проблема представления данных: множества, бинарные разрешающие диаграммы, конъюктивные нормальные формы … - Лекция За пределами логики дерева вычислений: мю-исчисление, его выразительная сила и алгоритмические свойства. Пример верификация мини-операционной системы, написанной на НеМо.

• Некоторые современные проблемы теории и технологии трансляции, анализа и верификации - Лекция За пределами модельного языка НеМо: рекурсия и динамические массивы, динамические переменные и указатели, динамическая память и безопасное программирование, объектно-ориентированное программирование.

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

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

- Лекция Современные инструментальные средства функционального подхода к трансляции: Lex и Yacc.

- Лекция Объектно-ориентированный подход к проектированию трансляторов.

- Лекция Верифицирующий транслятор для НеМо – это просто! Сертификация и интеграция переносимого кода – путь к созданию реального верифицирующего компилятора.

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

3 Учебно-методическое обеспечение дисциплины 3.1 Темы рефератов Не предусмотрено.

3.2 Образцы вопросов для подготовки к экзамену 3.3 Список основной и дополнительной литературы.

1. А.Ахо, Дж.Ульман. Теория синтаксического анализа, перевода и компиляции, 2 тома. М.:Мир, 1978.

2. А.Ахо, Р.Сети, Дж.Ульман. Компиляторы: принципы, технологии и инструменты. М.: Издательский дом ''Вильямc'', 2001.

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

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

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

6. П.Г.Емельянов. Абстрактная интерпретация императивных программ. В сб. Системная Информатика, Вып.6. Новосибирск: Наука, 1998. стр.7-47.

7. К.Ии, Н.В.Шилов, Е.В.Бодин. О программных логиках – просто. В сб. Системная Информатика, Вып.8.

Новосибирск: Наука, 2002.– С.206-249.

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

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

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

3.4 Для изучения дисциплин, которые предусматривают использование нормативно-правовых актов, указывать источник опубликования.

Не предусмотрено.