P.A. Shapkin1, A.N. Inozemtsev2

1–2 National Research Nuclear University MEPhI (Moscow, Russia)

1 pashapkin@mephi.ru, 2 inozemtsev.alex@outlook.com

Ins the process of modern software systems developing, their verification is carried out both statically and dynamically. Statically – by checking types during compilation. Dynamically – by testing. Dynamic verification has to be resorted to due to the limitations of the type systems of applied programming languages, which do not allow for comprehensive formal verification. At the same time, there are programming languages ​​and automated theorem proving systems that support full static formal verification of programs due to powerful type and logic inference systems, but it requires to additionally develop complex proofs of correctness that complement the main program code. Thus, the issue of combined use of dynamic and static verification capabilities is relevant.

One of the options for such interaction is to present specifications in the form of abstract structures that can be interpreted both as tests and as type expressions. The availability of such interpreters supporting various languages and proof systems will allow to combine dynamic testing with logical inference of specifications: if the programming language is not equipped with comprehensive static verification tools, then part of the specification can be verified dynamically, and another part can be proved in the automated proof system.

This paper considers a tool for interpreting specifications written in an abstract language as definitions of the Coq automated proof system. The purpose of translating specifications into Coq is their further use in formal inference. The result is a designed and implemented module for translating abstract specifications into the Coq language while preserving the semantics embedded in abstract specification constructor functions. The practical significance of the presented approach follows from the significance of software verification. The use of formal inference in verification allows one to avoid the need to test some specifications, due to the obvious limitations that arise during testing, even on a large set of input data. If the specification translation module is considered within the framework of a verification system, where there are translators of specifications into expressions for testing frameworks, in particular, random property-based testing, then its task is to combine tested specifications as premises in theorems that can be subsequently proven by formal inference.

Shapkin P.A., Inozemtsev A.N. Combined system for logical inference and dynamic verification of software component specifications. Information-measuring and Control Systems. 2024. V. 22. № 5. P. 69−79. DOI: https://doi.org/10.18127/j20700814-202405-08 (in Russian)

1. Hughes J. QuickCheck Testing for Fun and Profit. 2007. T. 4354. S. 1−32.
2. Claessen K., Hughes J. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming. New York. NY. USA: Association for Computing Machinery. 2000. S. 268−279.
3. Paraskevopoulou Z. et al. Foundational Property-Based Testing. 2015. T. 9236.
4. Lampropoulos L., Paraskevopoulou Z., Pierce B.C. Generating Good Generators for Inductive Relations. Proc. ACM Program. Lang. New York. NY. USA: Association for Computing Machinery. 2017. T. 2. № POPL.
5. Shapkin P.A. Sistema verifitsiruemykh spetsifikatsii programmnykh komponentov s podderzhkoi vstraivaniya i izvlecheniya. Programmnye produkty i sistemy. 2025. № 1. (in Russian)
6. Morten Heine Sorensen P.U. Lectures on the Curry-Howard Isomorphism. Elsevier Science. 2006.
7. Bruijn N.G. The Mathematical Language Automath, its Usage, and Some of its Extensions. Selected Papers on Automath. Editors R.P. Nederpelt, J.H. Geuvers, R.C. de Vrijer. Elsevier. 1994. T. 133. S. 73−100.
8. Marić F. A Survey of Interactive Theorem Proving. Zbornik radova. 2015.
9. Beringer L., Appel A. Abstraction and Subsumption. Modular Verification of C Programs. 2019. S. 573−590.
10. El Bakouny Y., Mezher D. The Scallina Grammar. Formal Methods: Foundations and Applications (editors Massoni T., Mousavi M.R.). Cham: Springer International Publishing. 2018. S. 90−108.
11. Annenkov D. et al. Extracting functional programs from Coq, in Coq. CoRR. 2021. T. abs/2108.02995.
12. Anand A. et al. Towards Certified Meta-Programming with Typed Template-Coq. Interactive Theorem Proving (editors Avigad J., Mahboubi A.) Cham: Springer International Publishing. 2018. S. 20−39.
13. Hudak P. et al. Report on the programming language Haskell: a non-strict, purely functional language version 1.2. SIGPLAN Notices. 1992. T. 27. S. 1.
14. Eisenberg R.A., Weirich S. Dependently typed programming with singletons. New York (USA): Association for Computing Machinery. 2012.