Шапкин П.А.1, Иноземцев А.Н.2

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

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

Постановка проблемы. При разработке современных информационных систем их верификация происходит статически (посредством проверки типов при компиляции) и динамически (с помощью тестирования). К динамической верификации приходится прибегать из-за ограниченности систем типов прикладных языков программирования, не позволяющей осуществлять исчерпывающую формальную верификацию. В то же время существуют языки программирования и системы автоматизированного доказательства теорем, поддерживающие полную формальную статическую верификацию программ за счет мощных систем типизации и логического вывода, но это требует разработки сложных доказательств корректности, дополняющих основной код программы. С учетом сказанного актуальной стала проблема совместного использования возможностей динамической и статической верификации. Один из вариантов такого взаимодействия состоит в представлении спецификаций в виде абстрактных структур, которые могут быть интерпретированы как в виде тестов, так и в ти́повые выражения. Наличия подобных интерпретаторов, поддерживающих различные языки и системы доказательства, позволит совмещать динамическое тестирование с логическим выводом спецификаций: если язык программирования не оснащен исчерпывающими средствами статической верификации, то часть спецификации может быть верифицирована динамически, а другая часть доказана в системе автоматизированного доказательства.

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

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

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

Шапкин П.А., Иноземцев А.Н. Совмещенная система логического вывода и динамической верификации спецификаций программных компонентов // Информационно-измерительные и управляющие системы. 2024. Т. 22. № 5. С. 69−79. DOI: https://doi.org/10.18127/j20700814-202405-08

1. Hughes J. QuickCheck Testing for Fun and Profit. 2007. Т. 4354. С. 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. С. 268−279.
3. Paraskevopoulou Z. и др. Foundational Property-Based Testing. 2015. Т. 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. Т. 2. № POPL.
5. Шапкин П.А. Система верифицируемых спецификаций программных компонентов с поддержкой встраивания и извлечения // Программные продукты и системы. 2025. № 1.
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. Т. 133. С. 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. С. 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. С. 90−108.
11. Annenkov D. и др. Extracting functional programs from Coq, in Coq // CoRR. 2021. Т. 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. С. 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. Т. 27. С. 1.
14. Eisenberg R.A., Weirich S. Dependently typed programming with singletons. New York (USA): Association for Computing Machinery. 2012.