Лейно Рустан - Доказательство корректности программ [2024, PDF, RUS]

Предисловие редактора................................................................................ 14
Вступление..................................................................................................... 16
Примечания для преподавателей............................................................... 22
Глава 0. Введение........................................................................................... 32
0.0. Предварительные сведения.......................................................................33
0.1. Краткое содержание книги.........................................................................35
0.2. Dafny............................................................................................................36
0.3. Другие языки...............................................................................................38
Часть 0. Знакомство с основами.................................................................. 39
Глава 1. Основы............................................................................................. 40
1.0. Методы.........................................................................................................40
1.1. Инструкции assert.......................................................................................41
1.2. Работа с верификатором............................................................................42
1.3. Пути потока управления............................................................................43
1.4. Контракты методов.....................................................................................45
1.4.0. Неполная спецификация...............................................................................46
1.4.1. Множественные постусловия.......................................................................48
1.5. Функции.......................................................................................................49
1.6. Компилируемые и призрачные конструкции...........................................51
1.6.0. Пример призрачного метода........................................................................52
1.7. Итоги............................................................................................................53
Глава 2. Добавляем формальности.............................................................. 57
2.0. Состояние программы................................................................................58
2.1. Логика Флойда.............................................................................................60
2.2. Тройки Хоара...............................................................................................62
2.3. Сильнейшие постусловия и слабейшие предусловия..............................64
2.3.0. Обмен местами значений переменных.......................................................66
2.3.1. Упрощение нотации доказательства корректности программы...............67
2.3.2. Одновременное присваивание.....................................................................69
2.3.3. Определение переменных............................................................................70
2.3.4. Осложнения....................................................................................................72
2.4. WP и SP........................................................................................................73
2.4.0. Обратный проход...........................................................................................73
2.4.1. Локальные переменные................................................................................74
2.5. Условное выполнение потока управления................................................74
2.5.0. Просто формулы, мэм...................................................................................76
2.6. Последовательная композиция.................................................................78
2.7. Вызовы методов и постусловия.................................................................80
2.7.0. Параметры......................................................................................................80
2.7.1. Предположения..............................................................................................81
2.7.2. Семантика вызова метода с постусловием..................................................81
2.8. Инструкции assert.......................................................................................84
2.8.0. Реальная разница между SP и WP................................................................85
2.8.1. Неофициальное чтение.................................................................................86
2.8.2. Использование assume для рассуждения о вызовах...................................87
2.9. Слабейшие свободные предусловия..........................................................87
2.9.0. Превращение обработки проверяемых условий в отдельную задачу.......88
2.9.1. Связь между WLP и SP...................................................................................89
2.9.2. Самое сильное консервативное постусловие? Такого не существует!......90
2.10. Вызовы методов с предусловиями..........................................................90
2.11. Вызовы функций.......................................................................................92
2.12. Частичные выражения..............................................................................93
2.13. Корректность метода................................................................................96
2.14. Итоги..........................................................................................................96
Глава 3. Рекурсия и завершимость.............................................................. 99
3.0. Бесконечная задача....................................................................................99
3.1. Как избежать бесконечной рекурсии......................................................102
3.2. Отношения полной фундированности....................................................107
3.3. Лексикографические кортежи..................................................................109
3.3.0. Оставшиеся предметы для изучения.........................................................110
3.3.1. Функция Аккермана....................................................................................111
3.3.2. Взаимно рекурсивные методы...................................................................112
3.3.3. Рефакторинг вложенных вычислений.......................................................114
3.4. Инструкции decreases по умолчанию......................................................117
3.5. Итоги..........................................................................................................118
Глава 4. Индуктивные типы данных......................................................... 120
4.0. Сине-желтые деревья...............................................................................121
4.1. Сопоставление типов данных..................................................................122
4.2. Дискриминаторы и деструкторы.............................................................124
4.3. Структурное включение...........................................................................125
4.4. Перечисления............................................................................................126
4.5. Параметры типа........................................................................................127
4.6. Абстрактные синтаксические деревья для выражений.........................128
4.7. Итоги..........................................................................................................132
Глава 5. Леммы и доказательства.............................................................. 134
5.0. Объявление леммы...................................................................................135
5.1. Использование леммы..............................................................................136
5.2. Доказательство леммы.............................................................................138
5.3. Назад к основам........................................................................................141
5.3.0. Доказательство с помощью логики Флойда..............................................141
5.3.1. Доказательства утверждений.....................................................................144
5.4. Доказательные вычисления.....................................................................146
5.4.0. Подсказки с использованием проверенных доказательств.....................148
5.5. Пример: Reduce.........................................................................................150
5.5.0. Верхняя граница..........................................................................................150
5.5.1. Нижняя граница...........................................................................................153
5.6. Пример: коммутативность умножения...................................................155
5.7. Пример: зеркальное отражение дерева...................................................158
5.7.0. Функция Mirror – это инволюция...............................................................158
5.7.1. Mirror сохраняет количество листьев.........................................................160
5.7.2. Варианты в доказательных вычислениях..................................................161
5.7.3. Итоги.............................................................................................................163
5.8. Пример: работа с абстрактными синтаксическими деревьями............164
5.8.0. Корректность определения подстановки...................................................164
5.8.1. Корректность определения оптимизации.................................................166
5.9. Итоги..........................................................................................................172
Часть I. Функциональные программы...................................................... 175
Глава 6. Списки............................................................................................ 176
6.0. Определение списка.................................................................................176
6.1. Length.........................................................................................................177
6.2. Внутренние и внешние характеристики.................................................178
6.2.0. Другие свойства Append..............................................................................180
6.3. Take и Drop................................................................................................182
6.4. At................................................................................................................183
6.5. Find.............................................................................................................186
6.6. Перестановка элементов списка в обратном порядке...........................187
6.7. Леммы в выражениях................................................................................192
6.7.0. Внутренняя спецификация ReverseAux......................................................192
6.7.1. Лемма об At и Reverse..................................................................................195
6.8. Исключение аргументов типа..................................................................198
6.9. Итоги..........................................................................................................199
Глава 7. Унарные числа............................................................................... 201
7.1. Основные определения.............................................................................201
7.2. Сравнения..................................................................................................202
7.2. Сложение и вычитание.............................................................................205
7.3. Умножение.................................................................................................207
7.4. Деление и остаток от деления..................................................................208
7.4.0. Доказательство завершимости через натуральные числа........................209
7.4.1. Доказательство завершимости посредством структурного включения....210
7.4.2. let-выражения с шаблонами........................................................................211
7.4.3. Корректность DivMod...................................................................................211
7.5. Итоги..........................................................................................................213
Глава 8. Сортировка.................................................................................... 216
8.0. Спецификация..........................................................................................216
8.0.0. Свойство упорядоченности.........................................................................216
8.0.1. Те же элементы............................................................................................218
8.0.2. Стабильность................................................................................................219
8.1. Сортировка вставками..............................................................................220
8.2. Сортировка слиянием...............................................................................222
8.2.0. Реализация...................................................................................................223
8.2.1. Корректность упорядоченности.................................................................225
8.2.2. Те же самые элементы.................................................................................227
8.3. Итоги..........................................................................................................230
Глава 9. Абстракция.................................................................................... 231
9.0. Группировка объявлений в модули.........................................................231
9.1. Импорт модулей........................................................................................232
9.2. Экспортируемые наборы..........................................................................233
9.3. Модульная спецификация очереди.........................................................236
9.3.0. Базовый интерфейс очереди......................................................................236
9.3.1. Функции абстракции...................................................................................237
9.3.2. Объявление экспортируемого набора........................................................239
9.3.3. Пример клиента...........................................................................................239
9.3.4. Реализация очереди....................................................................................241
9.4. Типы, поддерживающие оператор равенства.........................................244
9.4.0. Равенство......................................................................................................244
9.4.1. Разъяснение поддержки равенства............................................................245
9.4.2. Экспорт предиката IsEmpty.........................................................................245
9.5. Итоги..........................................................................................................247
Глава 10. Инварианты структур данных................................................... 249
10.0. Спецификация очереди с приоритетами..............................................250
10.0.0. Абстракция.................................................................................................250
10.0.1. Экспортируемый набор.............................................................................251
10.1. Проектирование структуры данных......................................................252
10.1.0. Допустимые деревья..................................................................................253
10.2. Реализация..............................................................................................254
10.2.0. Определение инварианта..........................................................................254
10.2.1. Пустая очередь...........................................................................................255
10.2.2. Вставка........................................................................................................256
10.2.3. Удаление наименьшего элемента.............................................................257
10.2.4. Вспомогательная функция DeleteMin......................................................258
10.2.5. Вспомогательная функция replaceRoot....................................................263
10.3. Создание внутренних спецификаций из внешних..............................266
10.3.0. Оптимизация DeleteMin............................................................................267
10.3.1. Спектр внутренних и внешних спецификаций.......................................268
10.3.2. Внешне внутренние и внутренне внешние спецификации...................269
10.4. Итоги........................................................................................................272
Часть II. Императивные программы......................................................... 275
Глава 11. Циклы........................................................................................... 276
11.0. Спецификации циклов...........................................................................276
11.0.0. Нетехнические примеры...........................................................................276
11.0.1. Логика Флойда для спецификаций циклов..............................................277
11.0.2. Числовые примеры....................................................................................278
11.0.3. Достижение равенства...............................................................................279
11.0.4. Отношения между переменными............................................................281
11.0.5. Фреймы циклов..........................................................................................282
11.1. Реализации циклов.................................................................................283
11.1.0. Деление с остатком....................................................................................283
11.1.1. Формальность в отношении сохранения инварианта цикла.................286
11.1.2. Вычисление сумм.......................................................................................287
11.1.3. Вывод фреймов цикла...............................................................................288
11.2. Завершимость цикла...............................................................................289
11.2.0. Завершимость деления с остатком...........................................................290
11.2.1. Инструкции decreases по умолчанию для циклов...................................292
11.3. В заключение о правилах оформления циклов....................................293
11.4. Целочисленный квадратный корень.....................................................295
11.4.0. Подход к решению задачи........................................................................295
11.4.1. Более эффективная программа................................................................296
11.5. Итоги........................................................................................................297
Глава 12. Рекурсивные спецификации, итеративные программы........ 299
12.0. Итеративное вычисление чисел Фибоначчи.........................................299
12.1. Квадрат числа Фибоначчи......................................................................303
12.1.0. Простое начало..........................................................................................303
12.1.2. Желание......................................................................................................304
12.1.2. Еще одно желание......................................................................................305
12.1.3. Рефлексия...................................................................................................306
12.2. Степени двойки.......................................................................................306
12.2.0. Обычный инвариант..................................................................................307
12.2.1. Альтернативный инвариант.....................................................................308
12.3. Суммы......................................................................................................310
12.3.0. Суммирование вверх и вниз.....................................................................310
12.3.1. Вычисление сумм итеративным способом..............................................312
12.3.2. Верификация суммирования....................................................................313
12.3.3. В заключение о программах суммирования...........................................314
12.4. Итоги........................................................................................................316
Глава 13. Массивы и поиск......................................................................... 317
13.0. О массивах...............................................................................................317
13.0.0. Размещение массива в памяти и его длина.............................................317
13.0.1. Элементы массива.....................................................................................318
13.0.2. Массивы являются ссылками....................................................................319
13.0.3. Многомерные массивы.............................................................................320
13.0.4. Последовательности..................................................................................320
13.1. Линейный поиск.....................................................................................322
13.1.0. Простая спецификация.............................................................................323
13.1.1. Необходимость оправдания неудачи.......................................................324
13.1.2. Поиск первого вхождения.........................................................................327
13.1.3. Зная, что искомый элемент существует...................................................327
13.1.4. Инвариант, указывающий, где искать......................................................329
13.1.5. В заключение о свойствах кванторов.......................................................330
13.2. Двоичный поиск......................................................................................331
13.2.0. Требование сортировки в спецификации................................................331
13.2.1. Постусловие двоичного поиска................................................................332
13.2.2. Реализация.................................................................................................333
13.3. Минимум.................................................................................................335
13.3.0. Наименьшее значение – единственное...................................................335
13.3.1. Наименьшее значение – не единственное..............................................336
13.3.2. Краткий обзор пройденного пути............................................................338
13.4. Количество совпадений..........................................................................338
13.4.0. Обозначения..............................................................................................339
13.4.1. Спецификация цикла................................................................................339
13.4.2. Тело цикла..................................................................................................340
13.4.3. Доказательство...........................................................................................341
13.4.4. Случай совпадения....................................................................................342
13.4.5. Первый случай несовпадения...................................................................343
13.4.6. Второй случай несовпадения....................................................................345
13.4.7. Краткий обзор пройденного пути............................................................345
13.5. Поиск точки на наклонной местности..................................................346
13.5.0. Начальная позиция поиска.......................................................................347
13.5.1. Реализация.................................................................................................348
13.6. Поиск каньона.........................................................................................349
13.6.0. Спецификация метода..............................................................................349
13.6.1. О каньоне...................................................................................................349
13.6.2. Реализация метода....................................................................................352
13.7. Голосование большинством....................................................................354
13.7.0. Подсчет вхождений....................................................................................354
13.7.1. Спецификация метода...............................................................................356
13.7.2. Разработка реализации.............................................................................357
13.7.3. Спецификация цикла.................................................................................358
13.7.4. Реализация цикла.......................................................................................358
13.7.5. Определение победителя, если он есть....................................................360
13.8. Итоги........................................................................................................364
Глава 14. Изменение массивов................................................................... 367
14.0. Простые фреймы.....................................................................................367
14.0.0. Инструкция modifies..................................................................................367
14.0.1. Старые значения........................................................................................369
14.0.2. Новые массивы..........................................................................................370
14.0.3. Свежие массивы.........................................................................................371
14.0.4. Инструкция reads.......................................................................................371
14.1. Простые изменения массивов...............................................................372
14.1.0. Инициализация массива...........................................................................372
14.1.1. Инициализация матрицы.........................................................................373
14.1.2. Увеличение значений в массиве...............................................................375
14.1.3. Копирование массива................................................................................377
14.1.4. Операции с массивами без циклов..........................................................379
14.2. Итоги........................................................................................................383
Глава 15. Сортировка на месте................................................................... 384
15.0. Голландский национальный флаг..........................................................384
15.1. Сортировка выбором..............................................................................388
15.2. Быстрая сортировка................................................................................391
15.2.0. Спецификация метода..............................................................................391
15.2.1. Предикаты с двумя состояниями.............................................................392
15.2.2. Основной алгоритм...................................................................................392
15.2.3. Использование SplitPoint..........................................................................393
15.2.4. Метод Partition...........................................................................................393
15.2.5. Реализация Partition..................................................................................394
15.3. Итоги........................................................................................................395
Глава 16. Объекты........................................................................................ 399
16.0. Контрольные суммы...............................................................................399
16.0.0. Спецификация...........................................................................................400
16.0.1. Тестовая программа..................................................................................401
16.0.2. Инвариант..................................................................................................402
16.0.3. Реализация.................................................................................................404
16.0.4. Модуль........................................................................................................405
16.0.5. Итоги...........................................................................................................406
16.1. Токенизатор.............................................................................................407
16.1.0. Синтаксические категории.......................................................................408
16.1.1. Класс и инвариант.....................................................................................408
16.1.2. Спецификация метода Read......................................................................409
16.1.3. Реализация Read........................................................................................412
16.2. Простые агрегатные объекты.................................................................413
16.2.0. Составляющие объекты с простыми фреймами......................................414
16.2.1. Версия 0 класса CoffeeMaker......................................................................415
16.2.2. Наборы представлений.............................................................................416
16.2.3. Реализация класса.....................................................................................419
16.2.4. Тестовая программа..................................................................................420
16.2.5. Технические характеристики Repr...........................................................421
16.2.6. Кратко об идиомах спецификаций..........................................................424
16.3. Сложные агрегатные объекты................................................................424
16.3.0. Составляющие объекты с динамическими фреймами...........................425
16.3.1. Инвариант CoffeeMaker: подмножества...................................................426
16.3.2. Два этапа выполнения конструкторов.....................................................426
16.3.3. Разделение наборов представлений........................................................427
16.3.4. Обновление Dispense.................................................................................432
16.4. Итоги........................................................................................................433
16.4.0. Набор представлений................................................................................433
16.4.1. Инвариант..................................................................................................433
16.4.2. Конструктор...............................................................................................434
16.4.3. Функции.....................................................................................................434
16.4.4. Методы.......................................................................................................434
Глава 17. Динамические структуры данных............................................. 437
17.0. Ленивая инициализация массивов........................................................437
17.0.0. Базовая спецификация..............................................................................437
17.0.1. Тестовая программа...................................................................................439
17.0.2. Неизменяемое состояние..........................................................................439
17.0.3. Базовая структура данных.........................................................................440
17.0.4. Инвариант объекта.....................................................................................442
17.0.5. Реализация.................................................................................................443
17.0.6. Доказательство, что в массиве есть место................................................444
17.1. Расширяемый массив..............................................................................446
17.1.0. Спецификация............................................................................................446
17.1.1. Структура данных......................................................................................447
17.1.2. Инвариант объекта.....................................................................................450
17.1.3. Реализация.................................................................................................451
17.1.4. Итоги...........................................................................................................454
17.2. Двоичное дерево поиска для ассоциативного массива........................454
17.2.0. Спецификация............................................................................................454
17.2.1. Реализация.................................................................................................455
17.2.2. Инвариант Node.........................................................................................456
17.2.3. Реализация Node........................................................................................458
17.2.4. Реализация Remove в классе Node............................................................461
17.3. Итератор для ассоциативного массива..................................................465
17.3.0. Спецификация............................................................................................465
17.3.1. Тестовая программа...................................................................................466
17.3.2. Стек оставшихся узлов...............................................................................467
17.3.3. Инвариант итератора.................................................................................468
17.3.4. Добавление узла в стек..............................................................................470
17.3.5. Конструктор................................................................................................473
17.3.6. Метод GetNext............................................................................................474
17.4. Итоги........................................................................................................475
Справочный материал................................................................................ 477
Приложение A. Синтаксис Dafny............................................................... 478
А.0. Объявления...............................................................................................478
А.0.0. Типы и объявления типов..........................................................................478
А.0.1. Объявления членов.....................................................................................479
А.1. Инструкции...............................................................................................480
А.2. Выражения................................................................................................482
Приложение B. Булева алгебра.................................................................. 485
B.0. Булевы значения и отрицание.................................................................485
B.1. Конъюнкция..............................................................................................485
B.2. Предикаты и корректность определений...............................................486
B.3. Дизъюнкция и правила доказательства..................................................487
B.4. Импликация..............................................................................................489
B.5. Доказательство истинности импликации..............................................490
B.6. Свободные переменные и подстановка..................................................492
B.7. Квантор всеобщности...............................................................................494
B.8. Квантор существования...........................................................................495
Приложение C. Решения некоторых упражнений................................... 499
Рекомендуемая литература....................................................................... 514
Предметный указатель............................................................................... 522