P.A. Shapkin¹, K.A. Legkodukh², E.D. Gajduk³

¹⁻³National Research Nuclear University MEPhI (Moscow, Russia)

¹pavel@shapkin.link

The object of the study is an abstract language of program specifications. Its interpretation of which generating test code or other specification representations. The subject of the study is to expand the expressive capabilities of the language by adding support for polymorphic constructs, as well as constructs that use the features of the object-oriented approach. The methods of applicative computing systems and type theory are used, providing a logical framework for both defining specifications and transforming them in the context of solving various problems. Verification of specifications through testing uses the random property-based testing approach.

The aim of this work is to develop a system for supporting polymorphism and object-oriented aspects in the system of abstract specifications of programs in the Scala language. This system should provide for the expansion of the functionality of the QuasiType library by integrating dynamic verification mechanisms and improving specification coverage evaluation algorithms. This approach is aimed at improving the quality and reliability of object-oriented software, as well as creating a basis for further research in the field of formal verification and specification of software systems.

The library’s functionality has been expanded by adding support for polymorphism and object-oriented aspects. The practical significance of the specification language being developed is that specifications themselves are standalone and are not directly represented as tests but can be interpreted as tests as well as other artifacts. The paper focuses on expanding the capabilities of the specification language, allowing a wider range of programs to be described.

Shapkin P.A., Legkodukh K.A., Gajduk E.D. Support for polymorphism and object-oriented aspects in the abstract program specification system. Information-measuring and Control Systems. 2025. V. 23. № 5. P. 86−94. DOI: https://doi.org/10.18127/j20700814-202505-09 (in Russian)

1. Shapkin P. Automation of Configuration, Initialization and Deployment of Applications Based on an Algebraic Approach. Procedia Computer Science. 2022. T. 213. S. 785−792.
2. Odersky M., Spoon L., Venners B. Programming in Scala. Artima Inc. 2008.
3. Shapkin P.A. Sistema verifitsiruemykh spetsifikatsii programmnykh komponentov s podderzhkoi vstraivaniya i izvlecheniya. Programmnye produkty i sistemy. 2025. T. 38. № 1. S. 65−76. (in Russian)
4. Bekkert B. Formalnye metody i programmnaya inzheneriya: 17‑ya Mezhdunar. konf. po formalnym inzhenernym metodam. Springer. 2015. (in Russian)
5. Volfengagen V.E. Metody i sredstva vychislenii s ob'ektami. Applikativnye vychislitelnye sistemy. M.: YurInfoR. 2004. (in Russian)
6. Volfengagen V.E. Kombinatornaya logika v programmirovanii. Vychisleniya s ob'ektami v primerakh i zadachakh. Izd. 3‑e, dopoln. i pererab. M.: Institut "YurInfoR MGU". 2008. (in Russian)
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. T. 19. № 5. S. 509−543.
10. Abadi M., Cardelli L. A theory of objects. Springer. Berlin. 1996.