Программа проверки корректности программного обеспечения

1. Формулировка проблемы 4
1.1 Введение 4
1.2 Актуальность проблемы 5
1.3 Существующие подходы к автоматизированному контролю корректности программного обеспечения 6
1.4 Контроль качества программного обеспечения на этапе создания 7
1.5 Контроль качества программного обеспечения на этапе выполнения10
1.6 Общая характеристика подходов 12
1.7 Постановка задачи 13
2. Контрактное программирование 15
2.1 Общие сведения о контрактном программировании 15
2.2 Библиотека Code Contracts 17
2.3 Предусловия 18
2.4 Постусловия 18
2.5 Инварианты класса 20
2.6 Контракты для интерфейсов 21
3. Темпоральные логики 23
3.1 Общие сведения о темпоральных логиках 23
3.2 Темпоральные операторы 23
3.3 Кванторы пути 25
3.4 Виды темпоральных логик 26
4. Предлагаемый подход 28
4.1 Структурная схема 28
4.2 Взгляд со стороны разработчика 28
4.3 Жизненный цикл программного продукта в сочетании с предлагаемым подходом 29
5. Сравнение подходов на примере класса Price 33
5.1 Без использования подходов контроля качества 35
5.2 На основе механизма исключений 36
5.3 На основе механизма контрактов 37
5.4 С использование предлагаемого подхода 38
5.5 Сравнение подходов и выводы 39
6. Инструменты работы с языком IL 41
6.1 Обзор языка IL 42
6.2 IL Disassembler 42
6.3 Microsoft.CCI 43
7. Архитектурное решение 45
7.1 Спецификация инструмента 45
7.2 Общее архитектурное решение 45
7.3 Архитектурное решение блока интеграции бизнес требований 47
7.4 Анализ .NET сборки 49
7.5 Преобразование бизнес-требования в TL формулу 52
7.6 Преобразование требований в IL код 55
8. Модификация IL кода на примере 59
9. Интеграция с бизнес-приложениями 66
10. Тестирование плагина 67
Заключение 73
Словарь сокращений 74
Краткий список основных инструкций языка IL 75
Список литературы 79
Приложение. Листинг исходного кода 80

Помимо теоретических обзоров и анализа предметной области, работа содержит результаты практического применения предложенного подхода в виде описания готового программного продукта. Приводится его структурная и архитектурная схема и ключевые алгоритмы работы. Большая часть работы посвящена разбору IL кода и методам его генерации.
В заключение в работе подводятся итоги исследований и исследуются перспективы дальнейшего развития метода и программного инструмента.
Данная работа посвящена такой острой проблеме современной ИТ-индустрии, как контроль качества программных продуктов (далее – ПО).

Суть данной дипломной работы – разработка инструмента, который бы позволял внедрять бизнес-требования в код и автоматически проверять их во время исполнения программы.