WWW.DISS.SELUK.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА
(Авторефераты, диссертации, методички, учебные программы, монографии)

 

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

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

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

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 Для изучения дисциплин, которые предусматривают использование нормативно-правовых актов, указывать источник опубликования.

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





Похожие работы:

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ Ярославский государственный университет им. П.Г. Демидова Экономический факультет УТВЕРЖДАЮ Проректор по развитию образования _Е.В.Сапир _2012 г. Рабочая программа дисциплины послевузовского профессионального образования (аспирантура) Современные проблемы экономической теории по специальности научных работников 08.00.01 Экономическая теория Ярославль 2012 2 1. Цели освоения дисциплины Целями освоения дисциплины Современные проблемы...»

«СИСТЕМА КАЧЕСТВА ПРОГРАММА ВСТУПИТЕЛЬНОГО ЭКЗАМЕНА В АСПИРАНТУРУ ПО СПЕЦИАЛЬНОСТИ 25.00.08 с. 2 из 10 ИНЖЕНЕРНАЯ ГЕОЛОГИЯ, МЕРЗЛОТОВЕДЕНИЕ И ГРУНТОВЕДЕНИЕ 1 ВВЕДЕНИЕ В соответствии с п. 40 Положения о подготовке научно-педагогических и научных кадров в системе послевузовского профессионального образования в Российской Федерации, утвержденного Приказом Министерства общего и профессионального образования от 27 марта 1998 г. № 814 (в редакции Приказов Минобразования РФ от 16.03.2000 № 780, от...»

«ФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ОБРАЗОВАНИЮ ГОСУДАРСТВЕННОЕ ОБРАЗОВАТЕЛЬНОЕ УЧРЕЖДЕНИЕ ВЫСШЕГО ПРОФЕССИОНАЛЬНОГО ОБРАЗОВАНИЯ ВОРОНЕЖСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ (ГОУ ВПО ВГУ) УТВЕРЖДАЮ Заведующий кафедрой международных отношений и регионоведения РАБОЧАЯ ПРОГРАММА 1. Шифр и наименование специальности/направления: 030701 Международные отношения 2. Уровень образования: высшее профессиональное (специалист) 3. Форма обучения: очная 4. Код и наименование дисциплины (в соответствии с Учебным планом):...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ Ярославский государственный университет им. П.Г. Демидова Экономический факультет УТВЕРЖДАЮ Проректор по развитию образования _Е.В.Сапир _2012 г. Рабочая программа дисциплины послевузовского профессионального образования (аспирантура) Маркетинг, логистика, стандартизация и управление качеством продукции, ценообразование по специальности научных работников 08.00.05 Экономика и управление народным хозяйством (по отраслям и сферам деятельности,...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РФ Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования Тверской государственный университет Физико-технический факультет Кафедра прикладной физики УТВЕРЖДАЮ Декан физико-технического факультета Педько Б.Б. _ 2012 г Рабочая программа по дисциплине Кристаллофизика для студентов 4 курса направление 222000.62 ИННОВАТИКА Профиль подготовки Управление инновациями (по отраслям и сферам экономики) Квалификация (степень)...»

«Приложение №1 к Положению о Тринадцатых молодежных Дельфийских играх России Программные требования конкурсной и фестивальной программ Тринадцатых молодежных Дельфийских игр России Репетиционное время участникам Игр гарантируется. Очередность выступлений определяется жеребьевкой. Все произведения исполняются наизусть. Соревнования по всем номинациям проводятся публично. Программа может быть исполнена полностью или частично по решению жюри. Выступления и работы, не соответствующие Программным...»

«2 1. Цель освоения дисциплины Расширить у магистрантов информационный рационалистический горизонт знаний, сформировать прогрессивный мировоззренческий подход к пониманию реальной картины мира, понимание концептуальных направлений развития науки. Сформировать у магистрантов комплекс понятий о специфике научного знания и методов науки, о глубокой связи науки и техники в современном информационном обществе, о главных задачах современной методологии науки, об истории развития науки. Задачи освоения...»

«Средства информатизации. Телекоммуникационные технологии, 2009, 256 страниц, Могилев Александр Владимирович, 5977501501, 9785977501507, БХВ-Петербург, 2009. Книга является частью комплекта учебных пособий по курсу информатики и информационнокоммуникационных технологий (ИКТ) в старших классах общеобразовательной школы на профильном уровне. Данное пособие охватывает содержание 3-го и 4-го из 10-ти модулей курса и дополняет изданные по курсу пособия Информация и информационные процессы. Социальная...»

«ОГЛАВЛЕНИЕ О программе AKVIS Pastel Установка программы под Windows Установка программы на Macintosh Регистрация программы Сравнение лицензий Работа с программой Рабочая область Работа с программой Инструменты и их параметры Параметры эффекта Надпись Работа с холстом Работа с пресетами Настройки программы Пакетная обработка Печать изображения Примеры Лебеди: танец на воде Программы компании AKVIS AKVIS Pastel РИСУНОК ПАСТЕЛЬЮ ИЗ ФОТОГРАФИИ   AKVIS Pastel...»

«ФГОС иннОвациОнная шкОла Программа курса БиОлОГия 5–9 классы линия Ракурс автор-составитель Н.И. романова 2-е издание Соответствует Федеральному государственному образовательному стандарту Москва Русское слово 2013 УДК 373.167.1:57* (073) ББК 74.262.8 П78 Автор-составитель Н.И. Романова Программа курса Биология. 5—9 классы. Линия П78 Ракурс/ авт.-сост. Н.И. Романова. — 2-е изд. — М.: ООО Русское слово — учебник, 2013. — 64 с. — (ФГОС. Инновационная школа). ISBN 978-5-00007-363-6 Программа...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования ТОБОЛЬСКАЯ ГОСУДАРСТВЕННАЯ СОЦИАЛЬНОПЕДАГОГИЧЕСКАЯ АКАДЕМИЯ ИМ. Д.И. МЕНДЕЛЕЕВА Кафедра математики, теории и методики обучения математике УМК УЧЕБНОЙ ДИСЦИПЛИНЫ СОВРЕМЕННЫЕ СРЕДСТВА ОЦЕНИВАНИЯ РЕЗУЛЬТАТОВ ОБУЧЕНИЯ Специальность 05020102 65 Математика (код и наименование направления подготовки) специализация Алгебра и геометрия Тобольск,...»

«КОММЕРЧЕСКИЙ ПОТЕНЦИАЛ НАУЧНЫХ РАЗРАБОТОК ННГУ Сборник информационно-аналитических материалов Нижний Новгород 2011 г. УДК 378.1 ББК Ч484 (2Р-4НН) 7Н.9 Т- К 63 Составители С.Н.Гурбатов, И.Я.Орлов, А.В.Калентьев, А.Е.Земсков, Ю.М.Максимов Под редакцией А.О.Грудзинского Т- К 63 Коммерческий потенциал научных разработок ННГУ. Сборник информационно-аналитических материалов – Н.Новгород: ННГУ им.Н.И.Лобачевского, 2011.- 61 стр. Публикуются материалы результатов исследования коммерческого потенциала...»

«1 Министерство сельского хозяйства Российской Федерации Федеральное государственное образовательное учреждение высшего профессионального образования Кубанский государственный аграрный университет РАБОЧАЯ ПРОГРАММА по дисциплине Б2.Б.3 Биологическая химия (индекс и наименование дисциплины) Специальность 110501.65 Ветеринарно-санитарная экспертиза Квалификация (степень) выпускника бакалавр Факультет Ветеринарной медицины Кафедра-разработчик Кафедра биохимии, биофизики и биотехнологии Ведущий...»

«Проект МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ Утвержден приказом Министерства образования и науки Российской Федерации от 200 г. № Регистрационный номер _ ФЕДЕРАЛЬНЫЙ ГОСУДАРСТВЕННЫЙ ОБРАЗОВАТЕЛЬНЫЙ СТАНДАРТ ВЫСШЕГО ПРОФЕССИОНАЛЬНОГО ОБРАЗОВАНИЯ по направлению подготовки 111200 – Ветеринария, специальность 111201 - Ветеринария Квалификация Ветеринарный врач Москва ОБЩИЕ ПОЛОЖЕНИЯ Направление подготовки 111200 – ветеринария, специальность 111201 – ветеринария, утверждены приказом...»

«Федеральное агентство связи Федеральное государственное образовательное бюджетное учреждение высшего профессионального образования Московский технический университет связи и информатики профиль Автоматизация технологических процессов и производств в почтовой связи Квалификация выпускника бакалавр Москва 2011 2 1. Общие положения 1.1. Определение Основная образовательная программа высшего профессионального образования (ООП ВПО) – система учебно-методических документов, сформированная на основе...»

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

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ УРАЛЬСКИЙ ГОСУДАРСТВЕННЫЙ ЭКОНОМИЧЕСКИЙ УНИВЕРСИТЕТ УТВЕРЖДАЮ Проректор по учебной работе Л. М. Капустина _2011 г. РЫНОК ТРУДА Программа учебной дисциплины 080101 ЭКОНОМИЧЕСКАЯ ТЕОРИЯ Квалификация (степень) выпускника Экономист Екатеринбург 2011 1. ЦЕЛИ ОСВОЕНИЯ УЧЕБНОЙ ДИСЦИПЛИНЫ Экономические преобразования в России требуют подготовки специалистов с новым типом экономического мышления, глубоко понимающих действие рыночного механизма,...»

«МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ ТОНКИХ ХИМИЧЕСКИХ ТЕХНОЛОГИЙ имени М.В. ЛОМОНОСОВА ФАКУЛЬТЕТ ХИМИИ И ТЕХНОЛОГИИ РЕДКИХ ЭЛЕМЕНТОВ И МАТЕРИАЛОВ ЭЛЕКТРОННОЙ ТЕХНИКИ АСПИРАНТУРА Программа кандидатского экзамена по 05.27.06 специальности 05.27.06 Технология и оборудование для производства полупроводников, материалов и приборов электронной техники УТВЕРЖДАЮ Ректор МИТХТ _А.К. Фролкова Протокол заседания Ученого Совета МИТХТ № 4 от 28.11. 2011г ПРОГРАММА КАНДИДАТСКОГО ЭКЗАМЕНА ПО СПЕЦИАЛЬНОСТИ...»

«Государственное бюджетное образовательное учреждение Среднего профессионального образования города Москвы Медицинское училище № 9 Департамента здравоохранения города Москвы (ГБОУ СПО МУ № 9 ДЗМ) Рабочая программа учебной дисциплины Генетика человека с основами медицинской генетики Наименование дисциплины 060501 Сестринское дело Код и наименование специальности, специальностей, группы специальности Базовый уровень среднего профессионального образования Уровень среднего профессионального...»

«Записи выполняются и используются в СО 1.004 СО 6.018 Предоставляется в СО 1.023. Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования Саратовский государственный аграрный университет имени Н.И. Вавилова Агрономический факультет СОГЛАСОВАНО УТВЕРЖДАЮ Декан факультета Проректор по учебной работе / Н.А. Шьюрова / _ /С. В. Ларионов/ _ _2013 г. _ _2013г. РАБОЧАЯ (МОДУЛЬНАЯ) ПРОГРАММА Дисциплина Основы биометода Для специальности 110203 растений...»






 
2014 www.av.disus.ru - «Бесплатная электронная библиотека - Авторефераты, Диссертации, Монографии, Программы»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.