Методы верификации программ
Покупка
Новинка
Тематика:
Программирование и алгоритмизация
Издательство:
ДМК Пресс
Автор:
Миронов Андрей Михайлович
Год издания: 2023
Кол-во страниц: 336
Дополнительно
Вид издания:
Учебное пособие
Уровень образования:
ВО - Бакалавриат
ISBN: 978-5-93700-278-5
Артикул: 856470.01.99
Доступ онлайн
999 ₽
В корзину
В книге излагаются вопросы моделирования и верификации (т.е. доказательства правильности) различных классов программ. Основные концепции и основанные на них подходы к верификации иллюстрированы примерами верификации различных программ. Для закрепления усвоения изложенного материала в книге приведено большое количество задач.
Книга предназначена для студентов высших учебных заведений, обучающихся по специальностям «теоретические основы информатики», «искусственный интеллект» и «информационная безопасность».
Тематика:
ББК:
УДК:
ОКСО:
- ВО - Бакалавриат
- 09.03.01: Информатика и вычислительная техника
- 09.03.02: Информационные системы и технологии
ГРНТИ:
Скопировать запись
Фрагмент текстового слоя документа размещен для индексирующих роботов
A. M. Миронов
МЕТОДЫ
ВЕРИФИКАЦИИ ПРОГРАММ
'издательство!
Москва, 2023
УДК 004.052
ББК 32.973.0
М64
Миронов А. М.
М64 Методы верификации программ. — М.: ДМК Пресс. 2023 — 336 с.
ISBN 978-5-93700-278-5
В книге излагаются вопросы моделирования и верификации (т.е. доказательства правильности) различных классов программ. Основные концепции и основанные на них под ходы к верификации иллюстрированы примерами верификации различных программ. Для закрепления усвоения изложенного материала в книге приведено большое количество задач.
Книга пред назначена д ля студентов высших учебных заведений, обучающихся по специальностям «теоретические основы информатики», «искусственный интеллект» и «информационная безопасность».
Книгаподготовлена при поддержке Междисциплинарнойнаучно-образовательной школы Московского университета «Мозг, когнитивные системы, искусственный интеллект».
УДК 004.052
ББК 32.973.0
Все права защищены. Любая часть этой книги не может быть воспроизведена в какой бы то ни было форме и какими бы то ни было средствами без письменного разрешения владельцев авторских прав.
Материал, изложенный в данной книге, многократно проверен. Но поскольку вероятность технических ошибок все равно существует, издательство не может гарантировать абсолютную точность и правильность приводимых сведений. В связи с этим издательство не несет ответственности за возможные ошибки, связанные с использованием книги.
ISBN 978-5-93700-278-5
© Миронов А. М., 2023
© Оформление, издание, ДМК Пресс, 2023
Оглавление
1 Введение 13
1.1 Проблема верификации программ................... 13
1.2 Необходимые математические понятия.............. 16
1.2.1 Термы и связанные с ними понятия.......... 16
1.2.2 Примеры типов и функциональных символов .... 18
1.2.3 Подстановки................................20
1.2.4 Массивы ...................................21
1.2.5 Истинностные значения утверждений..........22
I Верификация последовательных и распределённых программ 23
2 Программы, представленные в виде блок-схем 25
2.1 Понятие блок-схемы...............................25
2.2 Выполнение блок-схемы............................27
2.3 Примеры блок-схем................................28
2.4 Задача верификации блок-схем ....................31
3 Метод инвариантов для верификации блок-схем 33
3.1 Базовые множества и базовые пути.................33
3.2 Описание метода инвариантов......................34
3.3 Обоснование метода инвариантов...................35
3.4 Примеры фундированных множеств ..................36
3.5 Применение метода инвариантов ...................37
3.5.1 Верификация блок-схемы вычисления суммы .... 37
3.5.2 Верификация блок-схемы деления с остатком .... 39
3.5.3 Верификация блок-схемы извлечения корня.....40
3.5.4 Верификация блок-схемы возведения в степень ... 42
3.5.5 Верификация блок-схемы сортировки..........42
Оглавление
4 Процессные представления блок-схем 47
4.1 Понятие процесса...................................47
4.1.1 Действия.....................................47
4.1.2 Процессы и их выполнение.....................48
4.2 Процессы, соответствующие блок-схемам..............49
4.3 Верификация процессных представлений блок-схем.....50
5 Верификация операторных программ 53
5.1 Понятие операторной программы......................53
5.2 Примеры операторных программ.......................54
5.3 Метод инвариантов для верификации операторных программ ..................................................55
5.4 Пример верификации операторной программы...........56
6 Распределенные программы 59
6.1 Понятие распределенной программы...................59
6.1.1 Действия.....................................59
6.1.2 Процессы.....................................60
6.1.3 Распределенные программы.....................61
6.1.4 Каналы в распределенных программах...........61
6.1.5 Переходы в распределенных программах.........62
6.1.6 Выполнение распределенной программы..........64
6.2 Спецификация и верификация распределенных программ . 65
6.3 Примеры распределенных программ ...................66
6.3.1 Вычисление факториала........................66
6.3.2 Передача сообщений через буфер...............67
6.3.3 Избрание лидера..............................68
6.3.4 Параллельная сортировка......................69
6.4 Распределенная программа перемножения матриц.......70
6.4.1 Неформальное описание распределенной программы перемножения матриц 70
6.4.2 Спецификация программы перемножения матриц . . 70
6.4.3 Определение распределённой программы перемножения матриц 71
6.4.4 Дополненные процессы........................ 72
6.4.5 Верификация программы перемножения матриц . . 73
7 Задачи и исследовательские проблемы 79
7.1 Верификация программ без массивов................. 79
7.1.1 Произведение двух чисел..................... 79
7.1.2 Возведение в степень.........................80
Оглавление
5
7.1.3 Извлечение квадратного корня ...................80
7.1.4 Извлечение логарифма............................81
7.1.5 Вычисление частного и остатка от деления целых
чисел ..........................................81
7.1.6 Наибольший общий делитель.......................82
7.1.7 Представление наибольшего общего делителя линейной формой........................................84
7.1.8 Наибольший общий делитель и наименьшее общее
кратное.........................................84
7.1.9 Приближенное решение уравнения..................85
7.1.10 Проверка на простоту...........................85
7.1.11 Проверка, является ли число совершенным....86
7.2 Верификация программ с массивами......................86
7.2.1 Инвертирование массива..........................86
7.2.2 Минимальный элемент массива.....................87
7.2.3 Двоичный поиск..................................87
7.2.4 Наибольший общий делитель компонентов массива . 88
7.2.5 Список простых чисел от 2 до п..................88
7.2.6 Сортировка массива..............................89
7.2.7 Перестановка массива с заданным условием....90
7.2.8 Перестановка массива в заданном порядке.....90
7.2.9 Вычисление определителя матрицы.................91
7.3 Задачи на составление программ .......................92
7.4 Верификация распределенных программ...................94
7.5 Исследовательские проблемы ...........................95
II Верификация функциональных программ 97
8 Введение в функциональное программирование 99
8.1 Парадигма функционального программирования............99
8.2 Примеры функциональных программ......................100
8.2.1 Конкатенация строк.............................101
8.2.2 Инвертирование строки..........................101
8.2.3 Поиск подстроки................................102
9 Функциональные программы 103
9.1 Пополненные домены и функции на них..................103
9.1.1 Пополненные домены.............................103
9.1.2 Монотонные функции.............................103
9.1.3 Естественные продолжения.......................104
Оглавление
9.1.4 Частично упорядоченные множества монотонных функций .............................................105
9.1.5 Полные частично упорядоченные множества.....106
9.2 Функциональные программы..........................106
9.2.1 Понятие функциональной программы ...........106
9.2.2 Функционал, соответствующий функциональной программе ..........................................107
9.2.3 Непрерывные функционалы на полных частично упорядоченных множествах............................107
9.2.4 Неподвижные точки функционалов на полных частично упорядоченных множествах..................108
9.2.5 Непрерывность функционалов, соответствующих функциональным программам............................109
9.2.6 Нахождение наименьших неподвижных точек функциональных программ..............................112
9.2.7 Примеры неподвижных точек функциональных программ ...........................................113
9.2.8 Немонотонные функциональные программы.......114
9.3 Алгоритмическая полнота функциональных программ . . .115
10 Вычисление значений наименьших неподвижных точек 117
10.1 Постановка задачи................................117
10.2 Метод решения....................................117
10.3 Вычислительные правила...........................119
10.4 Упрощение терма..................................119
10.5 Функция Cs ......................................124
10.6 Вспомогательные понятия..........................126
10.6.1 Полные раскрытия ..........................126
10.6.2 Индексированные термы......................128
10.6.3 S-переходы.................................128
10.7 Безопасные вычислительные правила................131
10.8 Свойства правил РО, LO, PI, LI...................137
10.8.1 Безопасность правила РО ...................137
10.8.2 Безопасность правила LO....................139
10.8.3 Пример небезопасности правила LO...........141
10.8.4 Пример небезопасности правил PI и LI.......141
11 Верификация функциональных программ 143
11.1 Задача верификации функциональных программ.......143
11.2 Метод вычислительной индукции....................143
11.2.1 Описание метода............................143
Оглавление
7
11.2.2 Примеры верификации функциональных программ методом вычислительной индукции...................145
11.3 Метод структурной индукции.......................148
11.3.1 Описание метода............................148
11.3.2 Примеры верификации функциональных программ методом структурной индукции......................149
11.4 Другие методы верификации функциональных программ . 155
11.4.1 Оценка наименьшей неподвижной точки функциональной программы сверху..........................155
11.4.2 Эквивалентные преобразования функциональных программ ............................................156
12 Задачи и исследовательские проблемы 161
12.1 Нахождение наименьших неподвижных точек функциональных программ..........................................161
12.2 Вид наименьших неподвижных точек.................161
12.3 Функции, определяемые функциональными программами . 163
12.4 Свойства наименьших неподвижных точек............166
12.5 Исследовательские проблемы ......................169
III Model checking 171
13 Модели распределённых программ 173
13.1 Верификация распределённых программ..............173
13.1.1 Математические модели распределённых программ . 173
13.1.2 Спецификация...............................174
13.1.3 Построение формальных доказательств .......175
13.2 Системы переходов ...............................175
13.2.1 Понятие системы переходов..................176
13.2.2 Пути в системах переходов..................176
13.2.3 Построение системы переходов, соответствующей распределенной программе.............................177
14 Model checking на основе CTL 181
14.1 Темпоральная логика CTL..........................181
14.1.1 Формулы темпоральной логики CTL............181
14.1.2 Значения CTL-формул........................182
14.1.3 Эквивалентность CTL-формул.................182
14.1.4 Примеры свойств распределённых программ, выражаемых CTL-формулами..............................184
Оглавление
14.2 Задача model checking для CTL......................185
14.3 MC-CTL на основе понятия неподвижной точки.........186
14.3.1 Неподвижные точки монотонных операторов .... 186
14.3.2 Вычисление множеств (EU(B, С'))⁵' и (EGB)S на основе понятия неподвижной точки....................187
14.3.3 Алгоритм решения задачи MC-CTL на основе понятия неподвижной точки...............................190
14.4 //-исчисление......................................190
14.4.1 //-формулы...................................190
14.4.2 Значения //-формул...........................191
14.4.3 Ускоренное вычисление значений //-формул.....195
14.4.4 Вложение CTL в //-исчисление.................196
15 Бинарные диаграммы решений 199
15.1 Бинарные диаграммы решений и их свойства............199
15.1.1 Определение бинарной диаграммы решений.......199
15.1.2 Эквивалентность и изоморфность бинарных диаграмм решений.............................................200
15.1.3 Представление множеств замкнутых подстановок бинарными диаграммами решений.........................200
15.1.4 Редукция бинарных диаграмм решений...........201
15.1.5 Представление булевых функций................202
15.1.6 Подстановка значений вместо переменных.......202
15.2 Согласованность с порядком переменных..............203
15.3 Алгебраические операции на BDD.....................206
15.3.1 Булевы операции..............................206
15.3.2 Произведение.................................207
15.4 MC-CTL с использованием бинарных диаграмм решений . 209
15.5 Оптимизирующие преобразования......................211
16 Model checking на основе LTL 213
16.1 Формулы темпоральной логики LTL ....................213
16.2 Квантифицированные LTL-формулы.....................214
16.3 Задачи model checking для LTL......................215
16.3.1 Система переходов Бд.........................215
16.3.2 Система переходов S х Ед.....................217
16.3.3 Первая задача model checking для LTL.........219
16.3.4 Вторая задача model checking для LTL.........220
16.4 Автоматы Бюхи......................................223
16.4.1 Понятие автомата Бюхи .......................223
16.4.2 Язык автомата................................223
Оглавление
9
16.4.3 Эквивалентность автоматов...................224
16.4.4 Пересечение автоматов.......................225
16.4.5 Использование автоматов Бюхи для MC-LTL .... 226
16.4.6 Оптимизация построения автомата В а.........226
17 Вероятностный model checking 229
17.1 Введение..........................................229
17.2 Вероятностные системы переходов ..................230
17.2.1 Понятие вероятностной системы переходов.....230
17.2.2 Примеры вероятностных систем переходов......231
17.3 Темпоральная логика PCTL..........................233
17.3.1 Свойства вероятностных систем переходов.....233
17.3.2 Формулы логики PCTL.........................234
17.3.3 Значения формул логики PCTL в состояниях вероятностных систем переходов.........................234
17.3.4 Интерпретация значений формул логики PCTL . . . 236
18 Задачи и исследовательские проблемы 237
18.1 Задачи............................................237
18.2 Исследовательские проблемы .......................238
IV Теория процессов 241
19 Понятие процесса 243
19.1 Неформальное понятие процесса и примеры процессов . . . 243
19.1.1 Неформальное понятие процесса ..............243
19.1.2 Пример процесса.............................244
19.1.3 Другой пример процесса......................245
19.2 Действия..........................................246
19.3 Определение понятия процесса......................247
20 Операции на процессах 251
20.1 Префиксное действие...............................251
20.2 Пустой процесс....................................252
20.3 Альтернативная композиция.........................252
20.4 Параллельная композиция...........................255
20.5 Ограничение.......................................257
20.6 Переименование....................................259
20.7 Свойства операций на процессах...................259
Оглавление
21 Эквивалентности процессов 263
21.1 Простая эквивалентность.................................263
21.1.1 Поведение процесса................................263
21.1.2 Понятие простой эквивалентности...................264
21.1.3 Примеры процессов, находящихся в отношении простой эквивалентности................................264
21.2 Сильная эквивалентность.................................265
21.2.1 Понятие сильной эквивалентности ..................265
21.2.2 Критерий сильной эквивалентности, основанный на понятии бимоделирования.............................266
21.2.3 Логический критерий сильной эквивалентности . . . 268
21.2.4 Алгебраические свойства сильной эквивалентности . 270
21.2.5 Распознавание сильной эквивалентности........271
21.2.6 Минимизация процессов относительно сильной эквивалентности ......................................273
21.3 Наблюдаемая эквивалентность........................277
21.3.1 Определение наблюдаемой эквивалентности......277
21.3.2 Критерий наблюдаемой эквивалентности, основанный на понятии наблюдаемого бимоделирования . . 278
21.3.3 Логический критерий наблюдаемой эквивалентности процессов.......................................279
21.3.4 Алгебраические свойства наблюдаемой эквивалентности ..............................................279
21.3.5 Распознавание наблюдаемой эквивалентности .... 280
21.4 Наблюдаемая конгруэнция.................................281
21.4.1 Мотивировка наблюдаемой конгруэнции...............281
21.4.2 Определение наблюдаемой конгруэнции...............282
21.4.3 Связь между наблюдаемой эквивалентностью и наблюдаемой конгруэнцией ............................ 283
21.5 Другие эквивалентности процессов........................285
22 Примеры доказательства свойств процессов 287
22.1 Мастерская..............................................287
22.2 Планировщик.............................................289
23 Процессы с передачей сообщений 293
23.1 Действия с передачей сообщений .........................293
23.2 Процессы с передачей сообщений..........................293
23.2.1 Операторы.........................................293
23.2.2 Понятие процесса с передачей сообщений............294
23.2.3 Операции на процессах.............................295
Похожие
Доступ онлайн
999 ₽
В корзину