Данная работа посвящена изучению возможности применения подхода на основе типов-уточнений к анализу программ на языке Kotlin. Разработанный подход к выводу типов-уточнений использует информацию о путях исполнения функции для вывода типов-уточнений её аргументов. Вывод типов-уточнений выполняется за счёт построения системы ограниченных дизъюнктов Хорна и последующего её решения. В результате был реализован прототип системы, реализующей разработанный подход. Было проведено исследование качества работы прототипа, по результатам которого было принято решение о применимости созданного подхода.

This work is devoted to studying the possibility of using an approach based on refinement types to the analysis on Kotlin language programs. The developed approach to the refinement type inference infer refinement types for function arguments based on function execution paths. The inference of type refinements is carried out by constructing a system of constrained Horn clauses and its subsequent solution. As a result, a prototype system that implements the developed approach was implemented. The quality of the prototype was evaluated and the applicability of the created approach was decided according to the results.

• СПИСОК ОБОЗНАЧЕНИЙ И СОКРАЩЕНИЙ
• ВВЕДЕНИЕ
• 1. Обзор существующих решений
  • 1.1. Типы-уточнения
  • 1.2. Вывод типов-уточнений для ML подобных языков
    • 1.2.1. -исчисление и ML подобные языки
    • 1.2.2. Типы-уточнения общего назначения
    • 1.2.3. <<Жидкие>> типы
    • 1.2.4. Вывод с использованием интерполянтов
    • 1.2.5. Вывод типов-уточнений для функций высшего порядка
  • 1.3. Типы-уточнения для императивных языков
    • 1.3.1. Типы-уточнения для языка низкого уровня
    • 1.3.2. Типы-уточнения для объектно-ориентированного языка высокого уровня
  • 1.4. Резюме
• 2. Цели и задачи работы
  • 2.1. Задача вывода типов-уточнений для языка Kotlin
  • 2.2. Предлагаемый подход к заданию и выводу типов-уточнений
  • 2.3. Задача разработки прототипа системы вывода типов-уточнений для языка Kotlin
  • 2.4. Резюме
• 3. Описание подхода к выводу типов-уточнений
  • 3.1. Представление функции
    • 3.1.1. Predicate State
  • 3.2. Подготовка данных для вывода типов-уточнений
    • 3.2.1. Разрешение вложенных вызовов функций
    • 3.2.2. Подготовка для вывода типов-уточнений рекурсивных функций
  • 3.3. Вывод типов-уточнений
    • 3.3.1. Constrained Horn Clause
    • 3.3.2. Формализация задачи в виде системы CHC
    • 3.3.3. Построение типов-уточнений
  • 3.4. Ограничения разработанного подхода
  • 3.5. Резюме
• 4. Описание реализации прототипа
  • 4.1. Ручное задание типов-уточнений
  • 4.2. Представление в виде Predicate State
    • 4.2.1. Построение PS на основе исходного кода
    • 4.2.2. Построение PS на основе байткода JVM
  • 4.3. Подготовка данных для вывода типов-уточнений
  • 4.4. Построение и решение системы CHC
    • 4.4.1. Z3/Spacer
    • 4.4.2. Построение формулы SMT
    • 4.4.3. Построение CHC
    • 4.4.4. Решение системы CHC
  • 4.5. Формирование уточнения
  • 4.6. Ограничения реализованного прототипа
  • 4.7. Резюме
• 5. Тестирование и оценка результатов
  • 5.1. Методика тестирования
  • 5.2. Оценка результатов тестирования
    • 5.2.1. Анализ результатов работы прототипа
  • 5.3. Резюме
• ЗАКЛЮЧЕНИЕ
• СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ
• ПРИЛОЖЕНИЕ 1. ЛИСТИНГИ КОДА ПЛАГИНА ДЛЯ IDEA
• ПРИЛОЖЕНИЕ 2. ЛИСТИНГИ КОДА ВЫВОДА ТИПОВ-УТОЧНЕНИЙ