Алгоритмы вычисления отношений подобия в задачах верификации и реструктуризации программ

• Автор: Булычёв, Пётр Евгеньевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2010
• Место защиты: Москва
• Количество страниц: 169 с.

Оглавление
Введение
1. Проблема обнаружения программных клонов
2. Отношения симуляции между конечными автоматами (структурами Крипке)
3. Отношения симуляций между временными автоматами
Глава 1. Обнаружение подобных фрагментов в исходных кодах программ
1.1. Постановка задачи
1.2. Обзор методов и средств автоматического обнаружения клонов
1.3. Основные определения
1.4. Алгоритм поиска клонов
1.5. Теоретическое сравнение возможностей разработанного и существующих алгоритмов
1.6. Описание практической реализации
1.7. Результаты экспериментальных исследований
1.8. Область применимости
1.9. Заключение
Глава 2. Проверка отношений подобия между размеченными системами переходов (структурами Крипке)
2.1. Постановка задачи
2.2. Обзор литературы
2.3. Универсальный язык задания симуляций
2.4. Универсальный символьный алгоритм проверки симуляций

2.5. Описание практической реализации
2.6. Применение средства проверки симуляции для инкрементального построения модели
2.7. Область применимости
2.8. Заключение
Глава 3. Проверка отношений подобия между временными автоматами
3.1. Постановка задачи
3.2. Обзор существующих подходов
3.3. Определение слабой альтернирующей временной симуляции . .
3.4. Алгоритм проверки слабой альтернирующей временной симуляции
3.5. Описание практической реализации
3.6. Результаты экспериментальных исследований
3.7. Область применимости
Заключение
Литература
Приложение А. Руководство по использованию разработанных
программных средств
А.1. Запуск Clone Digger
А.2. Запуск универсальной среды проверки симуляции
Список иллюстраций
1.1 Фрагмент кода
1.2 Клон, удовлетворяющий определению, используемому в данной
работе, и его процедурная абстракция
1.3 Пример абстрактного синтаксического дерева (АСД)
1.4 Обычное и линеаризированное представление АСД
1.5 Пример бесполезного клона, обнаруженного на лексическом
уровне
1.6 Пример применения операции антиунификации
1.7 Алгоритм первого этапа кластеризации
1.8 Пример информации о клоне, обнаруженном средством Clone
Digger
1.9 Сравнение производительности Clone Digger и CloneDR
1.10 Количество всех найденных клонов и клонов, классифицированных вручную
1.11 Сравнение полноты обнаружения клонов
1.12 Сравнение точности обнаружения клонов
2.1 АД Astrong М
2.2 Верхние оценки сложности вычисления строгой и прореженной
симуляции и бисимуляции
2.3 Алгоритм решения игры
2.4 Пример игры для проверки прореженной симуляции
2.5 Алгоритм построения редуцированной игры
2.6 Алгоритм нахождения выигрышных состояний игрока Spoiler .
2.7 Результаты исследований на моделях универсального средства проверки симуляций, реализованного в рамках данной работы .
приводится алгоритм нахождения НСШ, который может быть применён не только к деревьям, но и к ориентированным графам без циклов.
1.3.2. Свойства наиболее специальных шаблонов НСШ как среднее значение множества деревьев
Легко видеть, что оператор антиунификации является коммутативным и ассоциативным, и, таким образом, его можно применять и к множеству деревьев. НСШ множества деревьев равен наиболее детализированному шаблону, которому удовлетворяют все деревья этого множества. Таким образом, он может восприниматься как “обшая форма”, равная общей верхней части всех деревьев множества. Это свойство антиунификации было использовано в работе [78] для нахождения классов часто встречающихся формул в математических текстах.
Расстояние по антиунификации
Пусть С — количество листьев дерева Т, помеченных символами-заполнителями и сг — количество остальных листьев. Определим размер дерева как [Т| = 0.5С1 +С2. Поясним, почему мы выбрали это определение. Размер абстрактного синтаксического дерева, определённый таким образом, инвариантен относительно способа представления фрагмента в виде АСД, поскольку он равен количеству вхождений всех имён и констант в программу. Например, фрагмент “а+-Ъ” может быть представлен как деревом — (о, Ь) так и деревом +(о, — (&)) (в зависимости от использования оптимизаций при построении АСД), но в обоих случаях количество листьев, помеченных метками-заполнителями равно С = 0 и количество остальных листьев равно сг = 2. Поэтому размер обоих этих деревьев будет равен О.бщ + сг = 2.