Детальная информация

Название: Типы-уточнения и их вывод для языка программирования Kotlin: выпускная квалификационная работа магистра: направление 09.04.01 «Информатика и вычислительная техника» ; образовательная программа 09.04.01_15 «Технологии проектирования системного и прикладного программного обеспечения»
Авторы: Соболь Валентин
Научный руководитель: Ицыксон Владимир Михайлович
Другие авторы: Новопашенный Андрей Гелиевич; Ахин Марат Халимович
Организация: Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий
Выходные сведения: Санкт-Петербург, 2020
Коллекция: Выпускные квалификационные работы; Общая коллекция
Тематика: типы-уточнения; Kotlin; ограниченные дизъюнкты Хорна; refinement types; constrained Horn clauses
Тип документа: Выпускная квалификационная работа магистра
Тип файла: PDF
Язык: Русский
Уровень высшего образования: Магистратура
Код специальности ФГОС: 09.04.01
Группа специальностей ФГОС: 090000 - Информатика и вычислительная техника
Ссылки: Отзыв руководителя; Рецензия; Отчет о проверке на объем и корректность внешних заимствований
DOI: 10.18720/SPBPU/3/2020/vr/vr20-771
Права доступа: Доступ по паролю из сети Интернет (чтение, печать, копирование)
Ключ записи: ru\spstu\vkr\6365

Разрешенные действия:

Действие 'Прочитать' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети Действие 'Загрузить' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети

Группа: Анонимные пользователи

Сеть: Интернет

Аннотация

Данная работа посвящена изучению возможности применения подхода на основе типов-уточнений к анализу программ на языке 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.

Права на использование объекта хранения

Место доступа Группа пользователей Действие
Локальная сеть ИБК СПбПУ Все Прочитать Печать Загрузить
Внешние организации №2 Все Прочитать
Внешние организации №1 Все
Интернет Авторизованные пользователи СПбПУ Прочитать Печать Загрузить
Интернет Авторизованные пользователи (не СПбПУ, №2) Прочитать
Интернет Авторизованные пользователи (не СПбПУ, №1)
-> Интернет Анонимные пользователи

Оглавление

  • СПИСОК ОБОЗНАЧЕНИЙ И СОКРАЩЕНИЙ
  • ВВЕДЕНИЕ
  • 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. ЛИСТИНГИ КОДА ВЫВОДА ТИПОВ-УТОЧНЕНИЙ

Статистика использования

stat Количество обращений: 22
За последние 30 дней: 0
Подробная статистика