Системы переписывания формул и их применение в автоматической верификации программ

• Автор: Ануреев, Игорь Сергеевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 1998
• Место защиты: Новосибирск
• Количество страниц: 135 с.

Содержание
Введение
1 Теория систем переписывания формул
§1 Основы теории систем переписывания термов
§1.1 Абстрактные системы редукций
§1.2 Системы переписывания термов
§1.3 Техника сужения
§2 Системы переписывания формул
§2.1 Основные определения
§2.2 Корректность систем переписывания формул
§2.3 Проблема нетеровости
§3 Завершимость систем переписывания формул
§3.1 Системы элиминации анализаторов
§3.2 Системы элиминации анализаторов со статусом
§3.3 Системы элиминации анализаторов с базой подстановок
2 Применение систем переписывания формул в автоматическом доказательстве
§1 Разрешимые теории
§1.1 Арифметика Пресбургсра и ее расширения
§1.2 Теории равенства и частичного порядка
§1.3 Теория равенства мультимножеств
§2 Особенности применения систем переписывания формул в многосортных теориях

§2.1 Сорта, определяемые обобщенными конструкторами :
§2.2 Корректность систем переписывания формул
§2.3 Булевский сорт
§3 Разрешающие процедуры, основанные на системах
переписывания формул
§3.1 Фрагменты теории целых чисел
§3.2 Фрагменты теории множеств
§3.3 Фрагменты теории мультимножеств
§3.4 Фрагменты теории кортежей
3 Применение систем переписывания формул в автоматической верификации программ
§1 Предварительные сведения о верификации
§1.1 Метод Хоара
§1.2 Система верификации СПЕКТР
§1.3 Модельный язык аннотированных программ
§2 Элиминация операций над структурами данных
§2.1 Последовательные файлы
§2.2 Массивы
§3 Модуль переписывания формул в системе СПЕКТР
§3.1 Общая структура модуля
§3.2 Тактикалы
§3.3 Результаты эксперимента
§4 Примеры автоматической верификации программ
§4.1 Программы редактирования текстов
§4.2 Сортировка массивов
§4.3 Сортировка файлов естественным слиянием
Заключение
Литература

Введение
В создании надежного программного обеспечения — важнейшей задачи технологии программирования — значительное место занимает классическая верификация программ [1, 21, 22, 31, 37, 73. 105, 132], основы которой были заложены в работах Флойда и Хо-ара. При этом решающую роль для автоматизации процесса верификации программ играет разработка методов автоматического доказательства, ориентированных на верификацию. Выделим методы и техники автоматического доказательства, которые используются в настоящее время в системах верификации. При рассмотрении методов и техник автоматического доказательства будем сравнивать их по следующим характеристикам:
- Ориентированность на верификацию, заключающаяся в том, учитывают ли разрешающие процедуры, основанные на том или ином методе или технике, специфику задачи верификации:
- Проблемная ориентированность, состоящая в том, могут ли разрешающие процедуры, основанные на том или ином методе или технике, использовать особенности конкретных проблемных областей чтобы проводить более эффективное доказательство:
- Классы формул, к которым применим метод или техника, и классы теорий, в рамках которых проводится доказательство.
Первую группу методов составляют универсальные методы [18. 20, 104], которые включают резолюцию [27, 36], обратный метод Маслова [26] и полные табличные методы [44, 103, 122]. Другие универсальные методы, основанные на том или ином исчислении и чисто дедуктивном выводе, не входят в эту группу, так как они не ориентированы на автоматическое доказательство. К досто-

переписывание кванторных формул определенного вида, а не на переписывание термов в эквивалентные термы, что имеет место при применении СПТ.
§2.3 Проблема нетеровости
Рассмотрим специальный класс СПФ — униформные системы, для которых подстановки фж — переименования. Таким образом, системы этого класса отличаются от обычных СПТ только разбором случаев, а для систем с единственной ветвью сводятся к обычным СПТ с точностью до переименования переменных. Поэтому ряд свойств СПТ переносится на униформные системы.
Определение. Пусть р — правило переписывания формул, тг — ветвь р. Ветвь я называется униформной, если I = в. Правило называется униформным, если униформны все ветви этого правила. СПФ Я называется униформной, если она состоит только из униформных правил.
Покажем, что проблема нетеровости неразрешима для униформных систем.
Теорема 3. Проблема нетеровости неразрешима для.униформных систем.
Доказательство. Будем доказывать от противного. Пусть существует алгоритм р, который проверяет, является униформная система нетеровой или нет. Покажем, что этот алгоритм можно использовать и для проверки свойства нетеровости для СПТ. состоящих из единственного правила. Пусть р — I —> г — правило переписывания термов. Возьмем униформное правило переписывания формул р' = ({/ —> г},1). Пусть Я'Р = ЫТ х ІІТ. Имеется следующая цепочка легко проверяемых тождеств:
р нетерово (—с)|щр нетерово;
(—>р)|щр нетерово (—>р')ь нетерово;