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

К. Рустан М. Лейно
Доказательство  
корректности программ

Program Proofs
K. Rustan M. Leino
Illustrated by Kaleb Leino
The MIT Press
Cambridge, Massachusetts
London, England

Москва, 2024
Доказательство  
корректности программ
К. Рустан М. Лейно
Иллюстрации: Калеб Лейно

УДК   004.052.42
ББК   32.973.2
Л42
Л42    К. Рустан М. Лейно
Доказательство корректности программ / Пер. с англ. А. Н. Киселева – 
М.: ДМК Пресс, 2024. – 530 с.: ил.
         ISBN 978-5-93700-199-3
Данная книга учит формально рассуждать о компьютерных программах, используя последовательный подход и язык программирования 
Dafny, поддерживающий верификацию. Показано, как писать спецификации для программ, как удовлетворить требования этих спецификаций и как писать доказательства корректности программ относительно 
спецификаций. Автор сначала представляет теоретические предпосылки, лежащие в основе рассуждений о программном коде, а затем постепенно переходит к реальным примерам, использующих объекты, структуры данных и нетривиальную рекурсию. Книга написана простым и 
понятным языком, содержит множество забавных иллюстраций и практических упражнений.
Издание будет полезно студентам вузов, преподавателям, исследователям в области формальной верификации, а также сотрудникам компаний, применяющих дедуктивную верификацию на практике.
© 2023 Massachusetts Institute of Technology. All rights reserved. Printed and bound in the 
United States of America. 
Все права защищены. Любая часть этой книги не может быть воспроизведена в какой бы то ни было форме и какими бы то ни было средствами без письменного разрешения 
владельцев авторских прав.
Материал, изложенный в данной книге, многократно проверен. Но, поскольку вероятность технических ошибок все равно существует, издательство не может гарантировать 
абсолютную точность и правильность приводимых сведений. В связи с этим издательство 
не несет ответственности за возможные ошибки, связанные с использованием книги.
ISBN 978-0-262-54623-2 (англ.)                   © Massachusetts Institute of Technology, 2023
ISBN 978-5-93700-199-3 (рус.)                     © Оформление, перевод на русский язык, 
	
                издание, ДМК Пресс, 2024

Оглавление
Предисловие редактора................................................................................ 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

6    Оглавление
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

Оглавление    7
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    Оглавление
Глава 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

Оглавление    9
Часть 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

10    Оглавление
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