Введение
1 К постановке основной задачи исследования 22
1.1 Библиографический обзор 1930-1989 гг. 23
1.1.1 Формальные модели вычислений 23
1.1.2 Аксиоматическая, операционная и денотационная семантика 26
1.1.3 Темпоральная логика и полиморфное Я-исчисление 27
1.1.4 Исчисление конструкций 29
1.1.5 Выводы по результатам библиографического обзора 31
1.2 Современное состояние исследований 32
1.2.1 Индуктивные и коиндуктивные типы (1990-е гг.) 33
1.2.2 Программирование с зависимыми типами (с 2000 г. по настоящее время) 34
1.2.3 Российские исследования 36
1.2.4 Выводы по современному состоянию исследований 38
1.3 Задача диссертационного исследования 39
1.3.1 Исследование и разработка математических моделей программ 40
1.3.2 Разработка макета языка и программного средства построения формальных моделей и верификации свойств программ 42
1.3.3 Исследование возможности использования макета программного средства для описания формальной семантики языков программирования 43
1.3.4 Исследование динамического параллельного исполнения программ 44
2 Математическая модель базового языка 46
2.1 Расширенное Исчисление Конструкций 46
2.1.1 Основные понятия 47
2.1.2 Типы суждений 50
2.1.3 Контекст 51
2.1.4 Тип 51
2.1.5 Зависимые произведения 52
2.1.6 Зависимые суммы 54
2.1.7 Свойства исчисления 55
2.1.8 Правила редукции 56
2.2 Исчисление с типами эквивалентности 57
2.2.1 Правила идентичности 59
2.2.2 Редукция — базовые правила 62
2.2.3 Эквивалентность — Туре 63
2.2.4 Эквивалентность на зависимых произведениях з
2.2.5 Эквивалентность на зависимых суммах 67
2.2.6 Эквивалентность — а =АЬ 69
2.2.7 Редукция в термах удаления 71
2.3 Выводы по второй главе 74
3 Разработка и реализация базового языка 76
3.1 Исчисление с индуктивными типами 76
3.1.1 Конечные типы 77
3.1.2 Натуральные числа 78
3.1.3 Высшие индуктивные типы 79
3.1.4 Индуктивные типы 82
3.1.5 Коиндуктивные типы 86
3.2 Реализация макета программного средства 88
3.2.1 Синтаксис 89
3.2.2 Основные конструкции 91
3.2.3 Преобразование в термы 93
3.2.4 Типизация 95
3.2.5 Частичный вывод типов 98
3.2.6 Особенности реализации 100
3.3 Выводы по третьей главе 102
4 Статическая семантика языков программирования 104
4.1 Стандарт ЕСМА-335 105
4.2 Разработка статической формальной семантики 1 4.2.1 Элементарные типы 109
4.2.2 Сборки, модули и типы данных 109
4.2.3 Пользовательские типы данных 111
4.2.4 Поля и методы 112
4.2.5 Окружения статической семантики 113
4.2.6 Тело метода 114
4.2.7 Семантика типизации 116
4.3 Динамическая семантика подмножества CIL 117
4.3.1 Монады и преобразователи монад 118
4.3.2 Модель чисел с плавающей точкой 121
4.3.3 Стек преобразователей монад динамической семантики 122
4.3.4 Динамическая семантика инструкций 124
4.3.5 Формальная семантика фрагмента кода 128
4.4 Выводы по четвёртой главе 129
5 Модель динамического параллельного исполнения программ 131
5.1 Язык управления потоком исполнения 134
5.2 Монада возобновлений и реактивный параллелизм 136
5.3 Модель динамического параллельного исполнения
5.3.1 Динамическая семантика языка управления потоком исполнения 139
5.3.2 Модель управляющего ядра системы 141
5.4 Свойства модели 145
5.4.1 Последовательный режим исполнения 145
5.4.2 Режим исполнения по требованию 150 5.5 Параллельное исполнение фрагмента кода 153
5.6 Выводы по пятой главе 154
Заключение 156
Список рисунков 158
Список таблиц 158
Список листингов 159
Литература
