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 | |
Language | Russian |
Level of education | Master |
Speciality code (FGOS) | 09.04.01 |
Speciality group (FGOS) | 090000 - Информатика и вычислительная техника |
Links | Отзыв руководителя ; Рецензия ; Отчет о проверке на объем и корректность внешних заимствований |
DOI | 10.18720/SPBPU/3/2020/vr/vr20-771 |
Rights | Доступ по паролю из сети Интернет (чтение, печать, копирование) |
Record key | ru\spstu\vkr\6365 |
Record create date | 7/2/2020 |
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 |
Данная работа посвящена изучению возможности применения подхода на основе типов-уточнений к анализу программ на языке 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.
Network | User group | Action |
---|---|---|
ILC SPbPU Local Network | All |
|
Internet | Authorized users SPbPU |
|
Internet | Anonymous |
|
- СПИСОК ОБОЗНАЧЕНИЙ И СОКРАЩЕНИЙ
- ВВЕДЕНИЕ
- 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. Резюме
- 3.1. Представление функции
- 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. ЛИСТИНГИ КОДА ВЫВОДА ТИПОВ-УТОЧНЕНИЙ
Access count: 42
Last 30 days: 0