Образцы вопросов для подготовки к экзамену

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

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

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

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

Формальные методы в программировании

Цели курса

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

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

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

№ п/п	Раздел дисциплины	Семестр	Неделя семестра	Виды учебной работы, включая самостоятельную работу студентов и трудоемкость (в часах)	Формы текущего контроля успеваемости (по неделям семестра) Форма промежуточной аттестации (по семестрам)
	Общее понятие программы
	Задача дедуктивной верификации
	Математические основы
	Язык исчисления вычислимых предикатов
	Система правил доказательства корректности программы							3 – Коллективная работа
	Построение языка предикатного программирования							3 - Контрольная
	Технология предикатного программирования							5 - Контрольная
	Язык, технология и методы верификации других классов программ

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

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

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

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

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

Классификация программ. Класс программ-функций.

Модель построения программы-функции. Логика решения.

Метод предикатного программирования на примере.

Логика программы. Логика выражений и базисных операторов. Корректность логики программы.

2) Задача дедуктивной верификации для класса невзаимодействующих программ

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

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

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

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

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

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

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

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

Структура программы: правила обозначения предикатов, вызов предиката, определение предиката.

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

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

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

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

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

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

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

Декомпозиция вхождений операторов в формулах корректности.

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

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

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

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

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

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

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

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

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

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

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

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

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

Гиперфункции. Проблемы реализации ветвления в программе. Определение гиперфункции и оператора продолжения ветвей. Определение предиката-гиперфункции. Спецификация предиката-гиперфункции. Синтаксические правила для оператора продолжения ветвей. Свойства гиперфункций. Построение программы «сумма чисел в строке». Использование гиперфункций в программе решения системы линейных уравнений.

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

8) Язык, технология и методы верификации других классов программ

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

Объектно-ориентированное расширение. Языковые конструкции. Инвариант класса. Условия корректности.

Автоматное программирование. Основные понятия: управляющие состояния, сегменты кода, состояние программы. Автоматная программа: конечный автомат в виде гиперграфа управляющих состояний. Языковые средства. Сообщения.

Декомпозиция простых процессов.

Пример: гадание на кофейных зернах. Пример: Электронные часы с будильником.

Реактивные и распределенные системы. Защищенный оператор. Сообщения и их виды.

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

Раздел 1.

1) Чем программа отличается от алгоритма?

2) Дать общее определение понятия программы.

3) Дать определение языка программирования и процессора языка программирования.

4) Назвать основные свойства программы.

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

6) Классификация программ. Класс программ-функций.

7) Определить модель разработки программы-функции. Логика решения.

8) Определить понятие логики программы. Определить логику выражений базисных операторов.

9) Дать определение корректности логики программы

10) Метод предикатного программирования на примере программы умножения через сложение.

11) Логика программы. Логика выражений и базисных операторов. Корректность логики программы.

Раздел 2

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

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

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

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

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

Раздел 3

17) Монотонные и непрерывные функции и их свойства.

18) Теорема Клини о наименьшей неподвижной точке.

19) Метод структурной и полной математической индукции. Индукция с использованием меры.

Раздел 4

20) Дать общее определение исчисления вычислимых предикатов

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

22) Описать систему типов данных: примитивные и структурные типы, подмножество типа, конструкторы и деструкторы.

23) Определить, что такое параметризация типов.

24) Определение рекурсивных типов. Определить тип последовательности.

25) Теория рекурсивных типов данных.

26) Логическая и операционная семантика операторов. Свойство согласованности.

27) Структура памяти исполняемой программы. Операции над секциями.

28) Вызов предиката. Лемма о согласованности вызова предиката.

29) Оператор суперпозиции. Лемма о согласованности оператора суперпозиции.

30) Параллельный оператор. Лемма о согласованности параллельного оператора.

31) Условный оператор. Лемма о согласованности условного оператора.

32) Конструктор предиката. Лемма о согласованности конструктора предиката.

33) Конструктор массива. Лемма о согласованности конструктора массива.

34) Структура программы на языке исчисления вычислимых предикатов.

35) Семантика рекурсивной системы определений предикатов.

36) Вычисление неподвижной точки. Структура рекурсивного кольца определений предикатов

37) Лемма о непрерывности оператора суперпозиции, параллельного оператора и условного оператора.

38) Теорема о согласованности логической и операционной семантики для программы на языке исчисления предикатов.

39) Свойства однозначных предикатов. Теорема однозначности программы.

Раздел 5.

40) Структура правила доказательства корректности; посылки, следствие. Правила для формулы тотальной корректности и теоремы тождества спецификации и программы.

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

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

43) Правило декомпозиции доказательства для оператора суперпозиции. Общий случай.

44) Правила декомпозиция вхождений операторов в формулах корректности.

45) Правило декомпозиции доказательства для параллельного оператора с корректными подоператорами.

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

47) Правило декомпозиции доказательства для оператора суперпозиции с корректными подоператорами.

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

49) Постановка задач верификации и синтеза предикатных программ.

Раздел 6.

50) Язык P1: подстановка определения предиката на место вызова. Операционная и логическая семантика.

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

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

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

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

55) Обобщение правил доказательства корректности операторов на случай рекурсии.

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

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

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

59) Способы описаний переменных в языке предикатного программирования.

60) Синтаксис и семантика определений типов в языке предикатного программирования.

61) Дать определение типа «подмножество». Определить понятие параметрического типа и его представления в языке предикатного программирования.

62) Алгебраические типы в языке предикатного программирования. Списки.

63) Массивы в языке предикатного программирования. Конструкции для работы с массивами.

64) Формулы в языке предикатного программирования.

65) Императивное расширение языка предикатного программирования. Цикл for. Групповой оператор присваивания и способ его раскрытия.

66) Модифицируемые переменные. Операторы, используемые для модифицируемых переменных.

Раздел 7.

67) Базовые трансформации предикатной программы.

68) Трансформация подстановки определения предиката на место вызова. Групповой оператор присваивания (мультиприсваивание) и способ его раскрытия.

69) Трансформация замены хвостовой рекурсии циклом

70) Трансформация склеивания переменных.

71) В чем заключается метод обобщения исходной задачи

72) Императивное расширение языка предикатного программирования.

73) Кодирование структурных типов. Методы кодирование списков через вырезки массива и с помощью указателей на примере программы суммирования элементов списка.

74) Кодирование списка указателями в программе обращения списка.

75) Программа сортировки простыми вставками. Оптимизация алгоритма. Построение императивной программы.

76) Проблемы реализации ветвления в программе. Определение гиперфункции и оператора продолжения ветвей.

77) Определение предиката-гиперфункции. Спецификация предиката-гиперфункции. Синтаксические правила для оператора продолжения ветвей. Свойства гиперфункций.

78) Система автоматизации доказательства PVS. Назначение, основные компоненты и принципы работы.

79) Типы и описания языка спецификаций системы PVS.

80) Формулы, теоремы и теории языка спецификаций системы PVS.

81) Генерация формул корректности в виде теорий на языке PVS на примере программ целочисленных стандартных функций.

Раздел 8.

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

83) Объектно-ориентированное расширение. Языковые конструкции. Инвариант класса. Условия корректности.

84) Автоматное программирование. Основные понятия: управляющие состояния, сегменты кода, состояние программы. Автоматная программа: конечный автомат в виде гиперграфа управляющих состояний.

85) Декомпозиция простых процессов. Спецификация простых процессов.

86) Класс реактивных и распределенных систем. Языковые средства. Защищенный оператор. Сообщения и их виды.

87) Пример: гадание на кофейных зернах.

88) Пример: Электронные часы с будильником.

89) Параллельная композиция процессов и ее спецификация на примерах протокола рукопожатия и алгоритма взаимного исключения Петерсона.

Дата добавления: 2015-06-27