Применение формальных методов для тестирования компиляторов

• Автор: Посыпкин, Михаил Анатольевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2004
• Место защиты: Москва
• Количество страниц: 155 с. : ил.

1 Обзор методов тестирования компиляторов. Постановка задачи

1.1 Основные понятия теории компиляции

1.2 Тестирование синтаксического анализатора

1.3 Тестирования фазы анализа статической семантики

1.4 Тестирование оптимизирующих преобразований в компиляторе

1.5 Тесты для проверки динамической семантики

1.6 Тестовые оракулы для фаз оптимизирующих преобразований и генерации кода

1.7 Постановка задачи

2 Базовые алгоритмы генерации тестовых программ для языка программирования

2.1 Описание подхода

2.2 Алгоритмы генерации тестов

2.3 Результаты главы
3 Генерация тестов для проверки реализации динамической семантики
3.1 Генерация строго конформных программ
3.2 Синтаксис и семантика языка Си5;тр1е
3.2.1 Язык Сих

3.2.2 Язык Сиг: Сиі + указатели
3.2.3 Язык Ciisimpie = Сиг + адресная арифметика, массивы и преобразования типов
3.3 Практическая апробация методики
3.4 Основные результаты главы
4 Критерии покрытия спецификаций семантики языка программирования
4.1 Система “Montages” описания семантики языков программирования
4.1.1 Формализм ASM
4.1.2 Монтажи как средство описания семантики языков программирования
4.2 Критерии покрытия Montage-спецификаций
4.2.1 Покрытие ASM-спецификаций
4.2.2 Комбинированный критерий покрытия
4.2.3 Критерий покрытия для семантических ограничений
4.3 Основные результаты главы
5 Опыт практического применения предложенной методики генерации тестов
5.1 Прототииная реализация генератора тестов и системы прогона тестов
5.2 Набор тестов для проверки реализации динамической семантики расширений, введенных стандартом Си 99
5.3 Тестирование компилятора с языка программирования трСЮЗ
5.3.1 Векторные и параллельные возможности языка трС105
5.3.2 Использование формализма Montages для определения семантики выражений трС
5.3.3 Результаты тестирования
5.3.4 Набор негативных тестов
5.4 Основные результаты главы

Заключение
А Подробное описание синтаксиса и семантики выражений шрС
А.1 Типы
АЛЛ Вектора
АЛ.2 Массивы
А.1.3 Указатели
АЛЛ Динамические типы
А.1.5 Контроль динамических типов
А.2 Преобразования типов
А.2.1 Классификация преобразований типов
А.2.2 Преобразования терминального типа
А.2.3 Конформные расширения
А.2.4 Преобразования типов операндов операций
А.З Последовательные выражения языка трС
А.3.1 Адресные вектора
А.3.2 Конструирование векторов
А.3.3 Операция приведения
А.3.4 Операция получения адреса
А.3.5 Операция косвенного доступа
А.З.6 Операции постфиксного инкремента и декремента
А.3.7 Операции префиксного инкремента и декремента
А.3.8 Другие унарные операции
А.З.9 Операции присваивания
А.3.10 Обращение к элементам массива
А.3.11 Обращение к элементам структур и объединений
А.З.12 Другие бинарные операции
А.4 Редуктивные операции
А.5 Параллельные выражения языка трС
А.5.1 Вычислительное пространство и сети
А.5.2 Распределенные объекты
А.5.3 Распределение вычислений

Рис. 2.2 Базовые алгоритмы генерации синтаксически и семантически корректных программ
algorithm GenerateSyntaxTests input: P, PN, PN = {{n)|n G PN}, i output: {s)i begin

forall nG N PN (n)o := 0 endforall do
forall n 6 N evaluate {n)j according to formulas (2.1) end forall
j :=j + 1 until j i return (s)i end
algorithm GenerateSemanticsTests input: P,PN, PN = {(ri)n G PN}, i output: at begin
(s)i := GencrateSyntaxTests(P, PN,FN,i)
:= 0 forall p G {s)i if § b p then