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

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