Сборники трудов ИСП РАН


Refinement типы для языка Jolie

Александр Чичигин (Университет Иннополис, Иннополис, Россия)
Лариса Сафина (Университет Иннополис, Иннополис, Россия)
Мохамед Эльвакиль (Университет Иннополис, Иннополис, Россия)
Мануэль Маццара (Университет Иннополис, Иннополис, Россия)
Фабрицио Монтези (Университет Иннополис, Иннополис, Россия)
Виктор Ривера (Университет Иннополис, Иннополис, Россия)

Аннотация

Jolie ¬— язык программирования для разработки микросервисов и на текущий момент является динамически проверяемым. В статье рассматривается возможность объединить динамическую и статическую проверку типов с помощью refinement типов, проверяемых SMT-решателем. Соединение этих двух аспектов делает возможным сценарий, когда статическая верификация внутренних сервисов и динамическая проверка (потенциально злонамеренных) внешних сервисов совместно снижают объёмы необходимого тестирования и увеличивают безопасность системы.
Refinement типы хорошо известны применительно к числовым типам данных, алгебраическим типам данных и массивам. Они основываются на соответствующих SMT теориях. Недавно SMT-решатели получили поддержку теории строк и регулярных выражений. В статье описывается возможность применения этой теории к строковым refinement типам. Мы используем язык программирования Jolie чтобы продемонстрировать целесообразность и полезность такого расширения. В первую очередь, потому что Jolie уже содержит синтаксическое расширение для строковых refinement типов. Мы развиваем указанное расширение, предоставляя статическую проверку типов. Во-вторых, поскольку в области микросервисов значение улучшенной проверки строковых данных гораздо выше, так как большинство коммуникаций с внешними системами происходит по текстовым протоколам.
Мы демонстрируем упрощённый, но реалистичный пример системы из области web-разработки. В пример преднамеренно внесена ошибка, показывая, как легко она ускользает от традиционной системы типов. Предложенное расширение целесообразно, поскольку оно не пропускает программу с ошибкой. Полноценное решение потребует доработки в части точности проверки и качества сообщений об ошибках.

Ключевые слова

Микросервисы, Jolie, Refinement типы, SMT, SAT, Z3

Издание

Труды Института системного программирования РАН, том 28, вып. 2, 2016, стр. 33-44.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(2)-2

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома