Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени



Скачать 75.55 Kb.
Дата07.11.2012
Размер75.55 Kb.
ТипПрограмма


Программа учебного курса
Предикатное программирование

    1. Цели и задачи курса

Цели курса

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

  • ознакомление студентов с практикой применения предикатного программирования.

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

    1. Новизна и актуальность курса


Построение эффективных и надежных программ ― актуальная проблема практического программирования. Предикатное программирование ― это новая парадигма, определяющая нетрадиционные методы в решении этой проблемы. Здесь сочетается математическое доказательство корректности программы и возможность построения эффективной программы. Предлагаемый курс определяет базисные концепции и методы предикатного программирования. Предикатное программирование позиционируется на границе между функциональным и логическим программированием. Предлагаемый курс не имеет аналогов в России и мире. Курс подготовлен по материалам публикаций и выступлений на семинарах в ИСИ и ИМ в 2001―2009гг.







п/п


Раздел

дисциплины

Семестр

Неделя семестра

Виды учебной работы, включая самостоятельную работу студентов и трудоемкость (в часах)

Формы текущего контроля успеваемости

(по неделям семестра)

Форма промежуточной аттестации

(по семестрам)

1

Общее понятие программы







2













2

Задача дедуктивной верификации







2













3

Математические основы







2













4

Язык исчисления вычислимых предикатов







6
















Система правил доказательства корректности программы







2










3 – Коллективная работа




Построение языка предикатного программирования







6










3 - Контрольная




Технология предикатного программирования







8










5 - Контрольная




Методы доказательства корректности программ







6

























36







11

47



    1. Содержание отдельных разделов и тем.

  1. Общее понятие программы

Понятие алгоритма и программы.

Свойство автоматической вычислимости программы.

Понятие языка программирования и процессора языка программирования.

Спецификация программы и ее основные свойства

Классификация форм спецификаций

Структура предикатной спецификации.

Логика программы. Примеры извлечения логики программы

  1. Задача дедуктивной верификации

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

Тотальная корректность программы.

Лемма о тотальности спецификации.

Теорема тождества спецификации и программы

Следствия теоремы тождества спецификации и программы

  1. Математические основы

Отношения порядка. Основные положения теории наименьшей неподвижной точки. Методы математической индукции.

  1. Язык исчисления вычислимых предикатов

Правила обозначения предикатов. Вызов предиката. Определение предиката.

Система типов данных. Примитивные и структурные типы данных. Подмножество типа. Конструкторы и деструкторы. Параметризация типов. Рекурсивные типы. Определение типа последовательности.

Семантика рекурсивных типов данных.

Логическая и операционная семантика операторов. Структура памяти предикатной программы. Операции над секциями. Вызов предиката и его исполнение. Оператор суперпозиции. Параллельный оператор. Условный оператор. Конструктор предиката. Конструктор массива. Доказательство свойства согласованности логической и операционной семантики операторов.

Программа на языке исчисления. Семантика рекурсивного кольца предикатов. Теорема согласованности логической и операционной семантики. Свойства однозначных предикатов. Теорема однозначности программы.

  1. Система правил доказательства корректности программы

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

Правила для общего случая. Правила для параллельного оператора. Правила для оператора суперпозиции. Правила для условного оператора.

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

Правила декомпозиции доказательства для общего случая. Правила для параллельного оператора. Правила для условного оператора. Правила для оператора суперпозиции.

Задачи верификации и синтеза.

  1. Построение языка предикатного программирования. Методы доказательства корректности предикатных программ

Язык P1: подстановка определения предиката на место вызова.

Язык P2: оператор суперпозиции и параллельный оператор общего вида. Семантика и правила доказательства корректности.

Язык P3: выражения. Функциональный и операторный стили. Правила доказательства корректности для вызова предиката с выражениями в качестве аргументов.

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

Конструкции языка. Лексика. Определение предиката. Основные операторы. Выражения. Описание переменных. Структура предикатной программы. Описание типов. Алгебраические типы. Списки. Массивы. Формулы. Императивное расширение языка предикатного программирования. Цикл for. Групповой оператор присваивания и способ его раскрытия.

Примеры предикатных программ.

  1. Технология предикатного программирования

Базовые трансформации предикатной программы. Подстановка определения предиката на место вызова. Замена хвостовой рекурсии циклом. Склеивание переменных. Метод обобщения исходной задачи. Кодирование структурных типов. Методы кодирование списков через вырезки массива на примере программы сортировки.

Определение гиперфункции и оператора продолжения ветвей. Логическая и операционная семантика. Определение предиката-гиперфункции. Спецификация предиката-гиперфункции. Синтаксические правила для оператора продолжения ветвей. Свойства гиперфункций. Правила доказательства корректности для предиката-гиперфункции.

Система автоматизации доказательства PVS. Назначение, основные компоненты и принципы работы. Типы и описания языка спецификаций системы PVS. Формулы, теоремы и теории языка спецификаций системы PVS. Генерация формул корректности в виде теорий на языке PVS.

Общее понятие верификации и валидации.

3.4. Список основной и дополнительной литературы

  1. Шелехов В.И. Предикатное программирование. Учебное пособие. — НГУ, Новосибирск, 2009. — 109с.

  2. Методы предикатного программирования. Вып.1— Сборник работ ИСИ СО РАН под ред. Шелехова В.И. — Новосибирск, 2003.

  3. Шелехов В.И. Разработка программы построения дерева суффиксов в технологии предикатного программирования. — Новосибирск, 2004. — 52с. — (Препр. / ИСИ СО РАН; N 115).

  4. Методы предикатного программирования. Вып.2— Сборник работ ИСИ СО РАН под ред. Шелехова В.И. — Новосибирск, 2006.

  5. Шелехов В.И. Модель корректности программ на языке исчисления вычислимых предикатов. — Новосибирск, 2007. — 50с. — (Препр. / ИСИ СО РАН; N 145).

  6. Шелехов В.И. Исчисление вычислимых предикатов. — Новосибирск, 2007. — 24с. — (Препр. / ИСИ СО РАН; N 143).

  7. Hoare C.A.R. Communicating Sequential Processes / Prentice-Hall.  1985.

  8. Milner R. A Calculus of Communicating Systems, Springer Verlag, ISBN 0387102353

  9. PVS System Guide. Version 2.4. — SRI International. 2001. — http://pvs.csl.sri.com/doc/pvs-system-guide.pdf

  10. PVS Language Reference. Version 2.4. — SRI International. 2001. — http://pvs.csl.sri.com/doc/pvs-language-reference.pdf

Программу подготовил Шелехов В.И.

Зав. лаб., к.т.н.



Похожие:

Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени iconПрограмма курса программирование
Гу-вшэ. Это – базовый курс программирования на языках высокого уровня для студентов, специализирующихся в области математики. Его...
Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени iconРабочая учебная программа Цели и задачи курса Тематический план курса Содержание программы по разделам
Ньютона; методы сопряженных направлений; численные методы решения задач вариационного исчисления и оптимального управления
Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени iconПлан лекций по биофизике для студентов первого курса педиатрического факультета (первый семестр) 2010-201 1 учебный год
...
Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени iconПрограмма по литургике для 2-го курса кдс I. Предмет и задачи учебного курса
Церкви. Задачи курса показать историю христианского богослужения, его эволюцию и существующие формы. Изучение чинопоследований суточного...
Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени iconЭлективный курс по химии в 10 классе «Решение задач повышенной трудности»
Цели: ознакомить учащихся с задачами курса; вспомнить и законспектировать основные законы химии, определить направление поиска методов...
Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени iconПояснительная записка цели и задачи изучаемого предмета ( курса) Изучение данного курса преследует триединую цель
Успешное освоение программы должно позволить слушателям эффективно решать следующие задачи
Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени iconМатричные способы решения задач школьного курса математики
Задачи школьного курса математики можно решить матричным способом. Матрица – прямоугольная или квадратная таблица, составленная из...
Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени iconЭлективный курс по математике «Метод математической индукции при решении задач»
Программа элективного курса «Метод математической индукции при решении задач» направлена на подготовку учащихся к предметной олимпиаде,...
Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени iconПарадигмы программирования
Цель курса систематизация знаний о возможностях и особенностях разных стилей и методов программирования при решении различных задач...
Учебного курса Предикатное программирование Цели и задачи курса Цели курса изучение теории и методов предикатного программирования для задач дискретной и вычислительной математики и задач реального времени iconФизическая защита ядерных объектов ( для группы Б01-43М ) Введение. Предмет, цели, задачи и содержание курса «Физическая защита ядерных объектов»
Предмет, цели, задачи и содержание курса «Физическая защита ядерных объектов» (фзяо). Роль и место курса в подготовке специалистов...
Разместите кнопку на своём сайте:
ru.convdocs.org


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