Программные продукты и системы

В настоящей работе описывается подход  к спецификации программных компонентов, реализованный автором в библиотеке Quasi-Type и дающий в зависимости от возможностей целевой среды отчуждаемые спецификации, оснащенные средствами погружения в различные вычислительные среды для дальнейшей динамической или статической верификации. Целью является выполнение таких задач, как верификация решений, построенных на нетипизированных компонентах, взаимодей- ствующих через интеграционное приложение на типизированном языке. В качестве примера может рассматриваться технология Scala.js, позволяющая использовать типизированный язык Scala для написания кода JavaScript (JS), нетипизированные внешние компоненты которого подключаются посредством типизированных оберток, или фасадов. Поскольку JS-код внешних компонентов недоступен для типизации, указанные в фасадах типы могут не соответствовать действительному поведению программы и требовать дополнительной верификации. При такой верификации объявленные структуры типов выступают в роли спецификаций, что приводит к необходимости решения задачи отображения типов на спецификации.
Подробное описание дается в статье "Система верифицируемых спецификаций программных компонентов с поддержкой встраивания и извлечения", автор Шапкин П.А. (Национальный исследовательский ядерный университет «МИФИ», г. Москва).