Экзамен

Экзаменационный билет состоит из двух вопросов по разным частям курса.
Для получения оценок «хорошо» и «отлично» необходимо ответить на дополнительные вопросы и/или решить предложенные задачи.

Вопросы к экзамену

Показательное множество. Отношения, функциональное отношение, частичная и тотальная функция. Рефлексивно-транзитивное замыкание. Отношение эквивалентности, фактормножество. Предпорядок. Частичный порядок, частично упорядоченное множество. Линейный порядок. Решетка.
Языки. Операции над языками. Грамматика и ее язык. Иерархия Хомского. Классы языков: конечные, регулярные, контекстно-свободные, рекурсивно перечислимые, рекурсивные, все языки. Отношение между ними.
Модели вычислений. Машина Тьюринга: определение, вычисление, язык, тотальность. Универсальная МТ.
Доказательство неразрешмости проблемы останова. Теорема Райса (формулировка для семантических свойств МТ, без доказательства).
Теорема об отсутствии идеального анализатора корректности МТ. Роль приближенных ответов в задачах анализа программ. Свойства анализатора: корректность, полнота, тотальность.
Синтаксис программы: конкретный и абстрактный. Лексический анализ. Расширенная форма Бэкуса-Наура. Дерево разбора грамматики. Абстрактные синтаксические деревья.
Семантика программы. Детерминированные программы. Операционная семантика (с малым шагом, большим шагом) и денотационная семантика.
Граф потока управления. Алгоритм его построения для последовательных императивных программ. Межпроцедурный CFG.
Частично упорядоченные множества и решетки: определение, свойства, характеристики, операции над ними, важные элементы, изоморфизм. Диаграмма Хассе. Конструкторы решеток: плоская решетка, показательная решетка, прямое произведение и степень, функциональная решетка.
Монотонные функции на решетках. Композиция монотонных функций. Теорема Клини о неподвижной точке. Наивный алгоритм поиска неподвижной точки и его вычислительная сложность.
Абстрактная интерпретация. Абстрактные домены. Соотношение Галуа.
Монотонные фреймворки на примере анализа знаков, анализа распространения констант и анализа ограниченных перечислений.
Монотонные фреймворки в компиляторах на примере анализа инициализированных переменных, живых переменных и доступных выражений. Направление анализа: вперед и назад. Анализ «may» и «must».
Алгоритмы поиска неподвижной точки: наивный, циклический, недетерминированный, простого рабочего списка. Вычислительная сложность этих алгоритмов.
Передаточные функции. Алгоритм простого рабочего списка и рабочего списка с распространением. Вычислительная сложность этих алгоритмов.
Сильно связные компоненты и конденсация графа. Топологическая сортировка, алгоритм ее построения. Оптимизация алгоритма поиска неподвижной точки в графе.
Интервальный домен: арифметика и сравнения. Интервальный анализ. Расширение и сужение.
Чувствительность анализа к путям выполнения. Метод использования операторов утверждений. Реляционный анализ. Контекст пути.
Межпроцедурный анализ. Наивный метод встраивания кода. Межпроцедурный граф потока управления.
Чувствительность анализа к контексту вызова. Строки вызова.
Анализ потоков управления. 0-CFA на примере λ-исчисления. Кубический алгоритм.

Примеры задач

Постройте абстрактное синтаксическое дерево и граф потока управления для заданной программы на модельном языке.
Функция f: L₁ → L₂, где L₁ и L₂ — решетки, называется дистрибутивной, если ∀ x, y ∈ L₁, f(x) ∨ f(y) = f(x ∨ y). Докажите, что каждая дистрибутивная функция является монотонной, но не каждая монотонная функция является дистрибутивной.
Докажите, что алгоритм рабочего списка, основанный на передаточных функциях, вычисляет то же решение, что и наивный алгоритм вычисления неподвижной точки.
Докажите изоморфизм декартовой степени решетки и функциональной решетки для конечной области определения.
Продемонстрируйте, каким образом ограничения анализа замыканий для λ-исчисления могут быть выражены как монотонные ограничения и решены алгоритмом вычисления неподвижной точки с соответствующим выбором решетки.