Details

Title: Типы-уточнения и их вывод для языка программирования Kotlin: выпускная квалификационная работа магистра: направление 09.04.01 «Информатика и вычислительная техника» ; образовательная программа 09.04.01_15 «Технологии проектирования системного и прикладного программного обеспечения»
Creators: Соболь Валентин
Scientific adviser: Ицыксон Владимир Михайлович
Other creators: Новопашенный Андрей Гелиевич; Ахин Марат Халимович
Organization: Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий
Imprint: Санкт-Петербург, 2020
Collection: Выпускные квалификационные работы; Общая коллекция
Subjects: типы-уточнения; Kotlin; ограниченные дизъюнкты Хорна; refinement types; constrained Horn clauses
Document type: Master graduation qualification work
File type: PDF
Language: Russian
Speciality code (FGOS): 09.04.01
Speciality group (FGOS): 090000 - Информатика и вычислительная техника
Links: Отзыв руководителя; Рецензия; Отчет о проверке на объем и корректность внешних заимствований
DOI: 10.18720/SPBPU/3/2020/vr/vr20-771
Rights: Доступ по паролю из сети Интернет (чтение, печать, копирование)

Allowed Actions:

Action 'Read' will be available if you login or access site from another network Action 'Download' will be available if you login or access site from another network

Group: Anonymous

Network: Internet

Annotation

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

Document access rights

Network User group Action
ILC SPbPU Local Network All Read Print Download
Internet Authorized users Read Print Download
-> Internet Anonymous

Table of Contents

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

Usage statistics

stat Access count: 2
Last 30 days: 0
Detailed usage statistics