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

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

Предисловие редактора
Вступление
Примечания для преподавателей
Глава 0. Введение
0.0. Предварительные сведения
0.1. Краткое содержание книги
0.2. Dafny
0.3. Другие языки
Часть 0. Знакомство с основами
Глава 1. Основы
1.0. Методы
1.1. Инструкции assert
1.2. Работа с верификатором
1.3. Пути потока управления
1.4. Контракты методов
1.4.0. Неполная спецификация
1.4.1. Множественные постусловия
1.5. Функции
1.6. Компилируемые и призрачные конструкции
1.6.0. Пример призрачного метода
1.7. Итоги
Глава 2. Добавляем формальности
2.0. Состояние программы
2.1. Логика Флойда
2.2. Тройки Хоара
2.3. Сильнейшие постусловия и слабейшие предусловия
2.3.0. Обмен местами значений переменных
2.3.1. Упрощение нотации доказательства корректности программы
2.3.2. Одновременное присваивание
2.3.3. Определение переменных
2.3.4. Осложнения
2.4. WP и SP
2.4.0. Обратный проход
2.4.1. Локальные переменные
2.5. Условное выполнение потока управления
2.5.0. Просто формулы, мэм
2.6. Последовательная композиция
2.7. Вызовы методов и постусловия
2.7.0. Параметры
2.7.1. Предположения
2.7.2. Семантика вызова метода с постусловием
2.8. Инструкции assert
2.8.0. Реальная разница между SP и WP
2.8.1. Неофициальное чтение
2.8.2. Использование assume для рассуждения о вызовах
2.9. Слабейшие свободные предусловия
2.9.0. Превращение обработки проверяемых условий в отдельную задачу
2.9.1. Связь между WLP и SP
2.9.2. Самое сильное консервативное постусловие? Такого не существует!
2.10. Вызовы методов с предусловиями
2.11. Вызовы функций
2.12. Частичные выражения
2.13. Корректность метода
2.14. Итоги
Глава 3. Рекурсия и завершимость
3.0. Бесконечная задача
3.1. Как избежать бесконечной рекурсии
3.2. Отношения полной фундированности
3.3. Лексикографические кортежи
3.3.0. Оставшиеся предметы для изучения
3.3.1. Функция Аккермана
3.3.2. Взаимно рекурсивные методы
3.3.3. Рефакторинг вложенных вычислений
3.4. Инструкции decreases по умолчанию
3.5. Итоги
Глава 4. Индуктивные типы данных
4.0. Сине-желтые деревья
4.1. Сопоставление типов данных
4.2. Дискриминаторы и деструкторы
4.3. Структурное включение
4.4. Перечисления
4.5. Параметры типа
4.6. Абстрактные синтаксические деревья для выражений
4.7. Итоги
Глава 5. Леммы и доказательства
5.0. Объявление леммы
5.1. Использование леммы
5.2. Доказательство леммы
5.3. Назад к основам
5.3.0. Доказательство с помощью логики Флойда
5.3.1. Доказательства утверждений
5.4. Доказательные вычисления
5.4.0. Подсказки с использованием проверенных доказательств
5.5. Пример: Reduce
5.5.0. Верхняя граница
5.5.1. Нижняя граница
5.6. Пример: коммутативность умножения
5.7. Пример: зеркальное отражение дерева
5.7.0. Функция Mirror – это инволюция
5.7.1. Mirror сохраняет количество листьев
5.7.2. Варианты в доказательных вычислениях
5.7.3. Итоги
5.8. Пример: работа с абстрактными синтаксическими деревьями
5.8.0. Корректность определения подстановки
5.8.1. Корректность определения оптимизации
5.9. Итоги
Часть I. Функциональные программы
Глава 6. Списки
6.0. Определение списка
6.1. Length
6.2. Внутренние и внешние характеристики
6.2.0. Другие свойства Append
6.3. Take и Drop
6.4. At
6.5. Find
6.6. Перестановка элементов списка в обратном порядке
6.7. Леммы в выражениях
6.7.0. Внутренняя спецификация ReverseAux
6.7.1. Лемма об At и Reverse
6.8. Исключение аргументов типа
6.9. Итоги
Глава 7. Унарные числа
7.1. Основные определения
7.2. Сравнения
7.2. Сложение и вычитание
7.3. Умножение
7.4. Деление и остаток от деления
7.4.0. Доказательство завершимости через натуральные числа
7.4.1. Доказательство завершимости посредством структурного включения
7.4.2. let-выражения с шаблонами
7.4.3. Корректность DivMod
7.5. Итоги
Глава 8. Сортировка
8.0. Спецификация
8.0.0. Свойство упорядоченности
8.0.1. Те же элементы
8.0.2. Стабильность
8.1. Сортировка вставками
8.2. Сортировка слиянием
8.2.0. Реализация
8.2.1. Корректность упорядоченности
8.2.2. Те же самые элементы
8.3. Итоги
Глава 9. Абстракция
9.0. Группировка объявлений в модули
9.1. Импорт модулей
9.2. Экспортируемые наборы
9.3. Модульная спецификация очереди
9.3.0. Базовый интерфейс очереди
9.3.1. Функции абстракции
9.3.2. Объявление экспортируемого набора
9.3.3. Пример клиента
9.3.4. Реализация очереди
9.4. Типы, поддерживающие оператор равенства
9.4.0. Равенство
9.4.1. Разъяснение поддержки равенства
9.4.2. Экспорт предиката IsEmpty
9.5. Итоги
Глава 10. Инварианты структур данных
10.0. Спецификация очереди с приоритетами
10.0.0. Абстракция
10.0.1. Экспортируемый набор
10.1. Проектирование структуры данных
10.1.0. Допустимые деревья
10.2. Реализация
10.2.0. Определение инварианта
10.2.1. Пустая очередь
10.2.2. Вставка
10.2.3. Удаление наименьшего элемента
10.2.4. Вспомогательная функция DeleteMin
10.2.5. Вспомогательная функция replaceRoot
10.3. Создание внутренних спецификаций из внешних
10.3.0. Оптимизация DeleteMin
10.3.1. Спектр внутренних и внешних спецификаций
10.3.2. Внешне внутренние и внутренне внешние спецификации
10.4. Итоги
Часть II. Императивные программы
Глава 11. Циклы
11.0. Спецификации циклов
11.0.0. Нетехнические примеры
11.0.1. Логика Флойда для спецификаций циклов
11.0.2. Числовые примеры
11.0.3. Достижение равенства
11.0.4. Отношения между переменными
11.0.5. Фреймы циклов
11.1. Реализации циклов
11.1.0. Деление с остатком
11.1.1. Формальность в отношении сохранения инварианта цикла
11.1.2. Вычисление сумм
11.1.3. Вывод фреймов цикла
11.2. Завершимость цикла
11.2.0. Завершимость деления с остатком
11.2.1. Инструкции decreases по умолчанию для циклов
11.3. В заключение о правилах оформления циклов
11.4. Целочисленный квадратный корень
11.4.0. Подход к решению задачи
11.4.1. Более эффективная программа
11.5. Итоги
Глава 12. Рекурсивные спецификации, итеративные программы
12.0. Итеративное вычисление чисел Фибоначчи
12.1. Квадрат числа Фибоначчи
12.1.0. Простое начало
12.1.2. Желание
12.1.2. Еще одно желание
12.1.3. Рефлексия
12.2. Степени двойки
12.2.0. Обычный инвариант
12.2.1. Альтернативный инвариант
12.3. Суммы
12.3.0. Суммирование вверх и вниз
12.3.1. Вычисление сумм итеративным способом
12.3.2. Верификация суммирования
12.3.3. В заключение о программах суммирования
12.4. Итоги
Глава 13. Массивы и поиск
13.0. О массивах
13.0.0. Размещение массива в памяти и его длина
13.0.1. Элементы массива
13.0.2. Массивы являются ссылками
13.0.3. Многомерные массивы
13.0.4. Последовательности
13.1. Линейный поиск
13.1.0. Простая спецификация
13.1.1. Необходимость оправдания неудачи
13.1.2. Поиск первого вхождения
13.1.3. Зная, что искомый элемент существует
13.1.4. Инвариант, указывающий, где искать
13.1.5. В заключение о свойствах кванторов
13.2. Двоичный поиск
13.2.0. Требование сортировки в спецификации
13.2.1. Постусловие двоичного поиска
13.2.2. Реализация
13.3. Минимум
13.3.0. Наименьшее значение – единственное
13.3.1. Наименьшее значение – не единственное
13.3.2. Краткий обзор пройденного пути
13.4. Количество совпадений
13.4.0. Обозначения
13.4.1. Спецификация цикла
13.4.2. Тело цикла
13.4.3. Доказательство
13.4.4. Случай совпадения
13.4.5. Первый случай несовпадения
13.4.6. Второй случай несовпадения
13.4.7. Краткий обзор пройденного пути
13.5. Поиск точки на наклонной местности
13.5.0. Начальная позиция поиска
13.5.1. Реализация
13.6. Поиск каньона
13.6.0. Спецификация метода
13.6.1. О каньоне
13.6.2. Реализация метода
13.7. Голосование большинством
13.7.0. Подсчет вхождений
13.7.1. Спецификация метода
13.7.2. Разработка реализации
13.7.3. Спецификация цикла
13.7.4. Реализация цикла
13.7.5. Определение победителя, если он есть
13.8. Итоги
Глава 14. Изменение массивов
14.0. Простые фреймы
14.0.0. Инструкция modifies
14.0.1. Старые значения
14.0.2. Новые массивы
14.0.3. Свежие массивы
14.0.4. Инструкция reads
14.1. Простые изменения массивов
14.1.0. Инициализация массива
14.1.1. Инициализация матрицы
14.1.2. Увеличение значений в массиве
14.1.3. Копирование массива
14.1.4. Операции с массивами без циклов
14.2. Итоги
Глава 15. Сортировка на месте
15.0. Голландский национальный флаг
15.1. Сортировка выбором
15.2. Быстрая сортировка
15.2.0. Спецификация метода
15.2.1. Предикаты с двумя состояниями
15.2.2. Основной алгоритм
15.2.3. Использование SplitPoint
15.2.4. Метод Partition
15.2.5. Реализация Partition
15.3. Итоги
Глава 16. Объекты
16.0. Контрольные суммы
16.0.0. Спецификация
16.0.1. Тестовая программа
16.0.2. Инвариант
16.0.3. Реализация
16.0.4. Модуль
16.0.5. Итоги
16.1. Токенизатор
16.1.0. Синтаксические категории
16.1.1. Класс и инвариант
16.1.2. Спецификация метода Read
16.1.3. Реализация Read
16.2. Простые агрегатные объекты
16.2.0. Составляющие объекты с простыми фреймами
16.2.1. Версия 0 класса CoffeeMaker
16.2.2. Наборы представлений
16.2.3. Реализация класса
16.2.4. Тестовая программа
16.2.5. Технические характеристики Repr
16.2.6. Кратко об идиомах спецификаций
16.3. Сложные агрегатные объекты
16.3.0. Составляющие объекты с динамическими фреймами
16.3.1. Инвариант CoffeeMaker: подмножества
16.3.2. Два этапа выполнения конструкторов
16.3.3. Разделение наборов представлений
16.3.4. Обновление Dispense
16.4. Итоги
16.4.0. Набор представлений
16.4.1. Инвариант
16.4.2. Конструктор
16.4.3. Функции
16.4.4. Методы
Глава 17. Динамические структуры данных
17.0. Ленивая инициализация массивов
17.0.0. Базовая спецификация
17.0.1. Тестовая программа
17.0.2. Неизменяемое состояние
17.0.3. Базовая структура данных
17.0.4. Инвариант объекта
17.0.5. Реализация
17.0.6. Доказательство, что в массиве есть место
17.1. Расширяемый массив
17.1.0. Спецификация
17.1.1. Структура данных
17.1.2. Инвариант объекта
17.1.3. Реализация
17.1.4. Итоги
17.2. Двоичное дерево поиска для ассоциативного массива
17.2.0. Спецификация
17.2.1. Реализация
17.2.2. Инвариант Node
17.2.3. Реализация Node
17.2.4. Реализация Remove в классе Node
17.3. Итератор для ассоциативного массива
17.3.0. Спецификация
17.3.1. Тестовая программа
17.3.2. Стек оставшихся узлов
17.3.3. Инвариант итератора
17.3.4. Добавление узла в стек
17.3.5. Конструктор
17.3.6. Метод GetNext
17.4. Итоги
Справочный материал
Приложение A. Синтаксис Dafny
А.0. Объявления
А.0.0. Типы и объявления типов
А.0.1. Объявления членов
А.1. Инструкции
А.2. Выражения
Приложение B. Булева алгебра
B.0. Булевы значения и отрицание
B.1. Конъюнкция
B.2. Предикаты и корректность определений
B.3. Дизъюнкция и правила доказательства
B.4. Импликация
B.5. Доказательство истинности импликации
B.6. Свободные переменные и подстановка
B.7. Квантор всеобщности
B.8. Квантор существования
Приложение C. Решения некоторых упражнений
Рекомендуемая литература
Предметный указатель