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

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