МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ
НОВОСИБИРСКИЙ ГОСУДАРСТВЕННЫЙ ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ
«УТВЕРЖДАЮ»
Проректор по учебной работе
_______________________
«__»____________ 2005 г.
Р А Б О Ч А Я П Р О Г Р А М М А
по дисциплине
«Теория вычислительных процессов»
подготовка бакалавров по направлению
552800 “Информатика и вычислительная техника”
специальность 220400 - “Программное обеспечение
вычислительной техники и автоматизированных систем”
Факультет Автоматики и вычислительной техники
Кафедра Автоматики
Курс 4 Семестр 7
Лекции 6 часа
Практические занятия 4 часа
Итого с преподавателем 10 часов
Контрольная работа 7 семестр
Экзамен 7 семестр
Новосибирск
2006
Рабочая программа составлена на основании Государственного образовательного стандарта высшего профессионального образования по направлению подготовки дипломированного специалиста 654600 «Информатика и вычислительная техника» (специальность 220400 – «Программное обеспечение вычислительной техники и автоматизированных систем». Стандарт утвержден 27.03.2000 г. Направление утверждено приказом Минобразования РФ г. Индекс СП.04.СД.05.
Регистрационный номер 224 тех/дс.
Рабочая программа обсуждена на заседании кафедры Автоматики, протокол № от г.
Программу составил
канд. техн. наук, ст. преп.
Заведующий кафедрой
д-р техн. наук, проф.
Эксперт НМЦ
канд. пед. наук., доц.
Ответственный за ООП
д-р техн. наук, проф.
1. Особенности курса
- Актуальность курса. Любой специалист в области программного обеспечения
вычислительной техники и автоматизированных систем должен иметь представление об основных принципах доказательства правильности программ для ЭВМ, а также о множестве задач, связанных с анализом, моделированием и представлением причинно-следственных связей в сложных системах параллельно действующих объектов. В рамках данного курса рассмотрены различные виды математической индукции, положенной в основу приемов доказательства правильности программ для вычислительных машин, а также приемы доказательства правильности программ, представленных блок-схемами или записанных на языках высокого уровня. Данный подход дает программисту некоторое систематическое средство для проверки его программ за столом, а также способствует более глубокому пониманию важнейших понятий программирования. Мощным средством решения задач моделирования систем являются сети Петри, методы построения и анализа которых рассмотрены во второй части курса. Курс входит в число дисциплин, включенных в учебный план направления в соответствии с ГОС. Данная дисциплина входит в цикл общематематических и естественнонаучных специальных дисциплин в соответствии с общеобразовательной программой базового высшего образования по направлению “Информатика и вычислительная техника”. Объем учебной работы и контроль изучения дисциплины(дневное отделение):
Факультет Автоматики и вычислительной техники
Кафедра Автоматики
Курс 4 Семестр 8
Лекции 34 часа
Практические занятия 34 часа
Самостоятельная работа 32 часа
Итого 100 часов
РГР 8 семестр
Экзамен 8 семестр
- Обучающийся данному курсу должен обладать знаниями основ программирования, математической логики, теории множеств, основ вычислительной техники, а также курсов “Теория формальных языков”, “Структуры и алгоритмы обработки данных” и “Системное программное обеспечение”. Курс адресован студентам, обучающимся по направлению 552800 “Информатика и вычислительная техника” и может быть полезен студентам других специальностей, изучающим программирование и интересующимся вопросами доказательства правильности программ и моделированием систем с помощью сетей Петри. Основная цель обучающихся – научиться доказывать правильность вычислительных процессов, представленных в виде блок-схем или программ, написанных на языках высокого уровня, а также использовать сети Петри как инструмент для моделирования аппаратного и программного обеспечения ЭВМ. Ядро курса – последовательное изучение приемов доказательства правильности программ и возможностей использования сетей Петри для моделирования и последующего анализа широкого класса систем, включающих параллельные действия. Курс имеет практическую часть – 32 часа практических занятий, включающих две самостоятельных работы, и расчетно-графическое задание из двух частей. Студенты применяют теоретические знания для доказательства правильности высказываний, блок-схем и программ, после чего исследуют возможности сетей Петри для моделирования широкого класса систем, представляющих взаимодействие различных процессов и проводят анализ моделируемых систем. Для освоения материала и выполнения расчетно-графического задания используются методические указания, учебные пособия и программное обеспечение, разработанное на кафедре «Автоматика». Оценка знаний и умений проводится по результатам работы на практических занятиях, выполнению заданий самостоятельных работ и РГР, а также по итоговому экзамену.
2. Цели и задачи изучения дисциплины,
ее место в учебном процессе
1. Цель изучения дисциплины
Данная дисциплина имеет целью:
1.1. Дать студентам знания, умения и навыки, необходимые для дальнейшей их деятельности, научить будущего специалиста инженерному мышлению, в том числе привить навыки в принятии решений по применению тех или иных методов верификации программного обеспечения;
1.2. Дать представление об организации вычислительных процессов, обеспечивающей наиболее эффективную работу вычислительных систем, верификации и моделировании процессов;
1.3. Научить студентов использовать методы анализа и синтеза программ, ознакомить с практическими принципами метода структурного программирования, использование которых позволяет не только создавать надежные и эффективные программы, но и доказывать их правильность путем логических рассуждений.
2. Место дисциплины в учебном процессе
Данная дисциплина входит в цикл общематематических и естественнонаучных специальных дисциплин в соответствии с общеобразовательной программой базового высшего образования по направлению “Информатика и вычислительная техника”. Дисциплина базируется знании таких дисциплин (на материале, изучаемом в курсах), как “Основы программирования”, “Математическая логика”, “Теория множеств”, “Основы вычислительной техники”, “Информатика и программирование”, “Системное программное обеспечение”, “Численные методы”.
3. Предметы изучения
3.1. Базовые определения и понятия вычислительных процессов и структурного программирования.
3.2. Структура и составные компоненты теории вычислительных процессов.
3.3. Взаимосвязь курса с другими научными дисциплинами и областями практической деятельности.
4. Объекты изучения
4.1. Базовые определения и понятия моделей вычислительных процессов.
4.2. Принципы и методы неформальной и формальной верификации программного обеспечения.
4.3. Способы организации вычислительных процессов в вычислительных системах.
4.4. Принципы построения и алгоритмы поведения сетей Петри.
5. Результаты изучения
5.1. Представления.
В результате изучения дисциплины у студентов должны быть сформированы представления об:
- методе математической индукции как способе, положенном в основу доказательства правильности программ; видах вычислительных процессов и их взаимодействии; принципах и методах структурного программирования; сетях Петри как математической модели систем.
5.2. Знания.
После изучения дисциплины студент должен приобрести знания в следующих областях:
- доказательство правильности программ; теория и практика структурного программирования; параллельные вычислительные процессы в вычислительных системах; сети Петри, способы их реализации и области применения.
5.3. Умения и навыки.
После изучения дисциплины студент должен:
- приобрести навыки в использовании метода индуктивных утверждений для доказательства правильности итеративных программ; уметь использовать принципы и методы структурного программирования для проектирования и верификации программ; ориентироваться в проблемах моделирования и синхронизации вычислительных процессов; уметь вести дискуссию в предметных областях, касающихся организации вычислительных процессов, проблем верификации программного обеспечения и сетей Петри.
6. Обязательный минимум содержания образовательной программы
СП.04 | Специальность “Программное обеспечение вычислительной техники и автоматизированных систем” | |
Индекс | Наименование и содержание дисциплины | Всего часов |
СД.05 | Теория вычислительных процессов Семантическая теория программ; схемы программ, методы формальной спецификации и верификации; модели вычислительных процессов; взаимодействие процессов; протоколы и интерфейсы; асинхронные процессы; сети Петри: принципы построения, алгоритмы поведения, способы реализации, области применения. | 100 |
3. Структура дисциплины
Содержание дисциплины соответствует программам курсов по теории вычислительных процессов, читаемых в высших технических учебных заведениях. Структура дисциплины состоит из двух основных разделов:
Доказательство правильности вычислительных процессов. Определяется предмет изучения, вводятся основная терминология, дается краткая историческая справка об основных направлениях исследований, связанных с доказательством правильности блок-схем и программ. Изучаются основные методы доказательства, особенности конструирования программ и языков, механизация процесса верификации, особенности доказательства правильности рекурсивных программ. Понятие моделирования. Модели параллельных вычислений. Сети Петри для моделирования. Основные определения, понятия, структура сетей Петри. Моделирование параллельных процессов, асинхронные процессы, механизмы синхронизации. Задачи и методы анализа сетей Петри. Расширения и ограничения сетей Петри.4. Содержание дисциплины
4.1. Лекционные занятия – 34 часа
Введение. Предмет, объект, метод, цель и задачи курса. Его связь с другими дисциплинами, формирующими специалистов по вычислительной технике. Программа курса и литература, предлагаемая для изучения, ее краткий анализ. – 0,5 час.
Тема 1. Математическая индукция. Введение: основные направления исследований, связанные с доказательством правильности программ (методы доказательства, конструирование программ и языков, механизация процесса доказательства правильности. Простая индукция: принцип простой индукции, принцип модифицированной простой индукции, доказательство высказываний, относящихся к программам для вычислительных машин. Строгая версия математической индукции: принцип строгой индукции. Обобщенная индукция: принцип обобщенной индукции. – 1,5 часа.
Тема 2. Доказательство правильности блок-схем программ. Основные принципы доказательства правильности для блок-схем. Понятие утверждения о правильности программ, инварианта цикла, утверждения о входных данных и утверждения о конечности программы. Дополнительные примеры доказательства правильности блок-схем программ. – 2 часа.
Тема 3. Метод индуктивных утверждений – основные определения и теоремы, описание метода. Частичная и полная правильность программы. Доказательство частичной правильности и конечности. Сокращенные доказательства правильности. – 2 часа.
Тема 4. Доказательство правильности программ, написанных на обычных языках программирования. Примеры доказательства правильности программ, написанных на Фортране. Примеры доказательства правильности программ, написанных на ПЛ/1. Особенности доказательства правильности программ, написанных на языках программирования visual basic и си. – 2 часа.
Тема 5. Формализация доказательства с помощью индуктивных утверждений. Аксиоматический подход к доказательству частичной правильности. Доказательство правильности как часть процесса программирования – 2 часа.
Тема 6. Доказательство правильности рекурсивных программ. Упрощенный язык программирования для иллюстрации понятия рекурсии. Структурная индукция. Более трудные примеры доказательства правильности программ методом структурной индукции. Структурная индукция для нерекурсивных программ. – 5 часов.
Тема 7. Современные исследования, связанные с доказательством правильности программ. Методы доказательства. Конструирование программ и языков. Механизация процесса доказательства правильности. – 1 час.
Тема 8. Сети Петри как инструмент моделирования систем. Введение. Литература. Понятие моделирования. Природа систем. Применение теории сетей Петри. Прикладная и чистая теории сетей Петри. – 1 час.
Тема 9. Основные определения и понятия. Структура сетей Петри. Графы сетей Петри. Маркировка сетей Петри. Правила выполнения сетей Петри. Пространство состояний сетей Петри. Альтернативные формы определения сетей Петри. – 3 часа.
Тема 10. Сети Петри для моделирования. Области применения сетей Петри. Принципы построения сетей Петри: события и условия, одновременность и конфликт аппаратного обеспечения ЭВМ: конечные автоматы, ЭВМ с конвейерной обработкой, кратные функциональные блоки. Моделирование сетями Петри программного обеспечения ЭВМ: блок-схемы, обеспечение параллелизма, задачи синхронизации. Другие системы с асинхронными параллельными взаимодействующими процессами. – 4 часа.
Тема 11. Задачи и методы анализа сетей Петри. Задачи анализа сетей Петри: безопасность, ограниченность, сохранение, активность, достижимость и покрываемость, эквивалентность и подмножество. Методы анализа сетей Петри. дерево достижимости, его построение и ограниченность применения, матричные уравнения. – 6 часов.
Тема 12. Расширенные и ограниченные модели сетей Петри. Границы возможностей моделирования с помощью сетей Петри. Взаимосвязь мощности моделирования и мощности разрешения. Виды расширений. Подклассы сетей Петри. – 2 часа.
Тема 13. Модели параллельных вычислений. Понятия эквивалентности и включения моделей. Соотношения между классами моделей и место сетей Петри в полной иерархии моделей. – 2 часа.
4.2. Практические занятия – 34 часа
1. Математическая индукция. – 2 часа.
2. Доказательство правильности блок-схем программ. – 2 часа.
3. Метод индуктивных утверждений. – 2 часа.
3. Доказательство правильности программ, написанных на обычных языках программирования. – 2 часа.
4. Формализация доказательства с помощью индуктивных утверждений. Аксиомы верификации для доказательства правильности. – 2 часа.
5. Рекурсивные программы. Работа со списками. – 2 часа.
6. Доказательство правильности рекурсивных программ. – 2 часа.
7. Самостоятельная работа (задачи по темам 1, 2, 4, 5, 6) – 2 часа.
8. Построение графов, инверсных и двойственных сетей Петри. – 2 часа.
9. Определение множества достижимости, последовательностей переходов и маркировок сетей Петри, моделирование реальной системы. – 2 часа.
10. Построение сетей Петри для конечных автоматов и блок-схем вычислительных процессов. – 2 часа.
11. Решение задач синхронизации: процессы чтения-записи и др. – 2 часа.
12. Задачи анализа свойств сетей Петри. – 2 часа.
13. Построение конечных и бесконечных деревьев достижимости – 2 часа.
14. Матричное представление сетей Петри, матричные уравнения – 2 часа.
15. Расширенные сети Петри: построение, анализ свойств. – 2 часа.
16. Самостоятельная работа (задачи по темам 10, 11, 12) – 2 часа.
17. Сравнительный анализ подклассов сетей Петри – 2 часа.
5. УЧЕБНО-МЕТОДИЧЕСКИЕ МАТЕРИАЛЫ ПО ДИСЦИПЛИНЕ
5.1 Основная и дополнительная литература
1. оказательство правильности программ. М.: Мир, 1982.
2. Веретельникова правильности программ: Метод индуктивных утверждений. Конспект лекций. Ч. 1. – Новосибирск, Изд-во НГТУ, 2004.
3. Веретельникова правильности программ: Дополнительные приемы. Конспект лекций. Ч. 2. – Новосибирск, Изд-во НГТУ, 2004.
4. Информатика. Теория и практика структурного программирования: Методическая разработка. – Новосибирск, изд-во НГТУ, 1999.
5. атематическая логика. – М.: Мир, 1973.
6. Котов Петри. – М.: Наука, 1984.
7. еория и практика структурного программирования. /Пер. с англ., М.: Мир, 1982.
8. Метод индуктивных утверждений для доказательства правильности программ: Учебное пособие. – Новосибирск, 2002. – В электронном виде.
9. Питерсон Дж. Теория сетей Петри и моделирование систем. – М.: Мир, 1984.
10. зык логики. – М.: Наука, 1969.
11. Хопкрофт Дж., Нльман Дж. Введение в теорию автоматов, языков и вычислений, 2-е изд. – М.: Изд. дом «Вильямс», 2002.
5.2. Использование средств ВТ
Для закрепления материала по теме «Сети Петри» в процессе самомтоятельной работы студенты могут пользоваться программой «Эмулятор сетей Петри», а также специализированными пакетами для моделирования систем с использованием сетей Петри, разработанными на кафедре автоматики НГТУ.
Контролирующие материалы
Приложение 1
Пример расчетно-графического задания
Вариант № 4
Часть 1. Тема
«Доказательство правильности методом индуктивных утверждений»
1. Для данной задачи составить блок-схему и доказать ее правильность методом индуктивных утверждений.
2. Для данной задачи написать программу на языке высокого уровня и доказать ее правильность. Доказательство проводить методом индуктивных утверждений, включая индуктивные утверждения в текст программы в виде комментариев.
Для матрицы AM×N найти наибольшую сумму элементов столбцов
Таблица вариантов
№ | задание |
1 | Для массива AM произвести сортировку элементов по возрастанию |
2 | Для матрицы AM×N найти наибольшую сумму элементов строк |
3 | Для матрицы AM×N найти наименьшую сумму элементов строк |
4 | Для матрицы AM×N найти наибольшую сумму элементов столбцов |
5 | Для матрицы AM×N найти наименьшую сумму элементов столбцов |
6 | Для матрицы AM×N найти сумму наибольших элементов строк |
7 | Для матрицы AM×N найти сумму наименьших элементов строк |
8 | Для матрицы AM×N найти сумму наибольших элементов столбцов |
9 | Для матрицы AM×N найти сумму наименьших элементов столбцов |
10 | Для матрицы AM×N найти наибольшее произведение элементов строк |
11 | Для матрицы AM×N найти наименьшее произведение элементов строк |
12 | Для матрицы AM×N найти наибольшее произведение элементов столбцов |
13 | Для матрицы AM×N найти наименьшее произведение элементов столбцов |
14 | Для матрицы AM×N найти произведение наибольших элементов строк |
15 | Для матрицы AM×N найти произведение наименьших элементов строк |
16 | Для матрицы AM×N найти произведение наибольших элементов столбцов |
17 | Для матрицы AM×N найти произведение наименьших элементов столбцов |
18 | Для матрицы AM×N найти наименьший элемент и среднее значение |
19 | Для матрицы AM×N найти наибольший элемент и среднее значение |
20 | Проверить матрицу AM×M на симметричность (установить значение переменной L=0 если А симметрична и L=1 в противном случае) |
21 | Проверить массивы AM и ВN на совпадение элементов (установить значение переменной L=0 если есть совпадающие элементы и L=1 в противном случае) |
22 | Для матрицы AM×N подсчитать количество элементов, равных 0 |
23 | Для матрицы AM×N, состоящей из чисел 0 и 1, заменить все 0 на 2 |
24 | Для матрицы AM×N подсчитать количество отрицательных элементов |
25 | Проверить матрицу AM×M, является ли она положительноопределенной (установить значение переменной L=0 если это так, и L=1 в противном случае) |
26 | Для матрицы AM×N подсчитать количество элементов |ai, j| < ε, где ε=0,1 |
27 | Для матрицы AM×N подсчитать количество отрицательных элементов |
28 | Проверить матрицу AM×M на наличие отрицательных элементов (установить значение переменной L=0 если это так, и L=1 в противном случае) |
29 | Для матрицы AM×N подсчитать количество положительных элементов |
30 | Для матрицы AM×N заменить отрицательные элементы их модулями |
Часть 2. Тема
«Основные понятия сетей Петри. Анализ сетей Петри»
Для предлагаемой сети Петри, заданной в виде двудольного ориентированного мультиграфа, выполнить следующее:
1) определить сеть Петри в виде C = (P, T, I, O);
2) определить расширенные входную и выходную функцию;
3) определить мультиграф в виде G = (V, A);
4) нарисовать граф инверсной сети Петри и описать ее как C = (P, T, I, O);
5) нарисовать граф двойственной сети Петри и описать ее как C = (P, T, I, O);
6) выполнить сеть Петри, записав последовательность переходов σ = tj1, …, tjk и последовательность маркировок μ0, …, μk ;
7) построить дерево достижимости и определить тип всех его вершин;
8) по дереву достижимости проверить свойства сети Петри: является ли она
а) безопасной, б) ограниченной, в) активной, г) строго сохраняющей;
9) для матричного представления сети Петри определить
матрицы D–, D+, D и вектор запусков последовательности f(σ) для σ из п.6.
Приложение 2
Экзаменационный билет № __6_____
По дисциплине Теория вычислительных процессов и структур
Факультет_____АВТФ_______________ Курс___4__________
Инварианты цикла при доказательстве правильности программ. доказательство правильности программ методом структурной индукции. Доказать, используя принцип простой математической индукции, что для любого положительного числа n справедлива приведенная ниже формула Составить блок-схему программы вычисления n! и доказать ее правильность
Приложение 3
Список экзаменационных вопросов
Математическая индукция. принципы простой индукции, модифицированной простой индукции, строгой индукции. Основные принципы доказательства правильности для блок-схем с использованием индукции. Инварианты цикла при доказательстве правильности. Метод индуктивных утверждений как обобщение метода доказательства правильности с использованием индукции. Частичная и полная правильность программы. Теорема о частичной правильности. Доказательство частичной и полной правильности как часть процесса программирования. Формализация доказательства с помощью индуктивных утверждений. Множество условий верификации. Доказательство правильности программ, написанных на языках программирования. Отличия от доказательства правильности блок-схем. Доказательство правильности программ, содержащих обращение к подпрограммам. Аксиоматический подход к доказательству частичной правильности и его идентичность методу индуктивных утверждений. Рекурсивные программы. Доказательство правильности рекурсивных программ методом структурной индукции. Моделирование. Природа моделируемых систем. Применение теории сетей Петри. Прикладная и чистая теории сетей Петри. Структура сетей Петри. Способы задания сетей Петри. Графы сетей Петри. Маркировка сетей Петри. Правила выполнения сетей Петри. Пространство состояний сетей Петри. События и условия. Моделирование процесса сетью Петри. Примитивные и не примитивные события. Одновременность и конфликт. Сети Петри для моделирования. Моделирование аппаратного обеспечения сетями Петри (конечные автоматы, ЭВМ с конвейерной обработкой, кратные функциональные блоки). Сети Петри для моделирования. Моделирование программного обеспечения сетями Петри (блок-схемы, обеспечение параллелизма). Сети Петри в решении задач синхронизации: задача о взаимном исключении, задача о производителе/потребителе, задача об обедающих мудрецах, задача о чтении/записи, P- и V-системы и др. Задачи анализа сетей Петри: безопасность, ограниченность, сохранение, активность, покрываемость. Дерево достижимости сети Петри. Использование дерева достижимости для анализа сетей Петри. Матричные уравнения и их использование для анализа сетей Петри. Сети Петри с ограничениями и подклассы сетей Петри. Расширенные модели сетей Петри (области ограничения, переходы исключающее ИЛИ, сети со сдерживающими дугами, сети с приоритетами, временные сети) Взаимосвязь мощности моделирования и мощности разрешения сетей Петри
