П.А. Шапкин¹, К.А. Легкодух², Е.Д. Гайдук³

¹⁻³Национальный исследовательский ядерный университет «МИФИ» (Москва, Россия)

¹pavel@shapkin.link

Постановка проблемы. Объектом исследования является абстрактный язык спецификации программ, интерпретация которых позволяет генерировать код тестов или других представлений спецификаций. Предметом исследования является расширение выразительных возможностей языка путем добавления в него поддержки полиморфных конструкций, а также конструкций, использующих особенности объектно-ориентированного подхода. Использованы методы аппликативных вычислительных систем и теории типов, дающие логический каркас как для определения спецификаций, так и для их преобразования в рамках решения различных задач. Проверка спецификаций посредством тестирования использует подход случайного тестирования на основе свойств.

Цель. Разработать системы поддержки полиморфизма и объектно-ориентированных аспектов в системе абстрактных спецификаций программ на языке Scala для расширения функциональности библиотеки QuasiType за счет интеграции механизмов динамической верификации и улучшения алгоритмов оценки покрытия спецификациями.

Результаты. Расширена функциональность библиотеки путем добавления поддержки полиморфизма и объектно-ориентированных аспектов. Достигнуто повышение качества и надежности объектно-ориентированного программного обеспечения. Созданы основы для дальнейших исследований в области формальной проверки и спецификации программных систем.

Практическая значимость. Разработанная система позволяет строить спецификации не только для конкретного применения с целью тестирования программ, но и для их дальнейшего преобразования путем построения композитных спецификаций и др. Рассматриваемое исследование расширяет возможности языка спецификаций, позволяя описывать более широкий спектр программ.

Шапкин П.А., Легкодух К.А., Гайдук Е.Д. Поддержка полиморфизма и объектно-ориентированных аспектов в системе абстрактных спецификаций программ // Информационно-измерительные и управляющие системы. 2025. Т. 23. № 5. С. 86−94. DOI: https://doi.org/10.18127/j20700814-202505-09

1. Shapkin P. Automation of Configuration, Initialization and Deployment of Applications Based on an Algebraic Approach // Procedia Computer Science. 2022. Т. 213. С. 785−792.
2. Odersky M., Spoon L., Venners B. Programming in Scala. Artima Inc. 2008.
3. Шапкин П.А. Система верифицируемых спецификаций программных компонентов с поддержкой встраивания и извлечения // Программные продукты и системы. 2025. Т. 38. № 1. С. 65−76.
4. Беккерт Б. Формальные методы и программная инженерия: 17‑я Междунар. конф. по формальным инженерным методам. Спрингер. 2015.
5. Вольфенгаген В.Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. М.: ЮрИнфоР. 2004.
6. Вольфенгаген В.Э. Комбинаторная логика в программировании. Вычисления с объектами в примерах и задачах. Изд. 3‑е, дополн. и перераб. М.: Институт «ЮрИнфоР МГУ». 2008.
7. Huth M., Ryan M. Logic in Computer Science: Modelling and Reasoning about Systems. Edition 2nd. Cambridge University Press. 2004.
8. Bernardo M. Formal Methods for Software Architectures: Third International School on Formal Methods for the Design of Computer, Communication, and Software Systems. Springer. 2003.
9. Carette J., Kiselyov O., Shan C. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages // Journal of Functional Programming (Cambridge University Press). 2009. Т. 19. № 5. С. 509−543.
10. Abadi M., Cardelli L. A theory of objects. Springer. Berlin. 1996.