Динамическая логика разделений и ее использование в образовании

  • Evgeny Maratovich Makarov Национальный исследовательский Нижегородский государственный университет им. Н.И. Лобачевского http://orcid.org/0000-0003-0399-0946

Аннотация

Математическая логика широко применяется для верификации программ и аппаратного обеспечения. Одной из логик, наиболее подходящих для верификации императивных программ, является логика Хоара. Ее расширение, логика разделений, использует разделяющую конъюнкцию, которая позволяет рассуждать о программах, использующих указатели и изменяемые структуры данных. Еще одним формализмом, используемым в верификации, является динамическая логика — частный случай модальной логики. Данная статья описывает пропозициональную динамическую логику разделений, которая добавляет разделяющую конъюнкцию к динамической логике.
Мы описываем синтаксис, семантику и исчисление в гильбертовском стиле для пропозициональной динамической логики разделений и доказываем ее корректность. Определение логики является достаточно абстрактным. Так, используемый язык программирования состоит из так называемых регулярных программ вместо программ с обычными конструкциями if и while. Множество атомарных программ может быть произвольным при условии, что они порождают локальные действия. Особое внимание уделяется корректности правила кадра, позволяющего писать локальные спецификации программ, то есть указывать участки памяти, которые непосредственно читаются или изменяются программой. Условные операторы также рассматриваются отлично от стандартной динамической логики.
Статья также содержит аргументы в пользу использования логики разделений в изучении компьютерных наук. Данная логика более проста, чем другие субструктурные логики, и может преподаваться даже в начальных курсах математический логики. В то же время, логика разделений является областью активных исследований с большим количеством применений. На основе этой логики построено много инструментов для верификации. Поэтому она является отличным введением в формальные методы.

Сведения об авторе

Evgeny Maratovich Makarov, Национальный исследовательский Нижегородский государственный университет им. Н.И. Лобачевского

старший преподаватель кафедры алгебры, геометрии и дискретной математики, Институт информационных технологий, математики и механики

Литература

[1] Upasani N., Om H. A modified neuro-fuzzy classifier and its parallel implementation on modern GPUs for real time intrusion detection. Applied Soft Computing. 2019; 82:105595. (In Eng.) DOI: https://doi.org/10.1016/j.asoc.2019.105595 Clarke E.M., Wing J.M. Formal methods: state of the art and future directions. ACM Computing Surveys. 1996; 28(4):626-643. (In Eng.) DOI: https://doi.org/10.1145/242223.242257
[2] Hoare C.A.R. An axiomatic basis for computer programming. Communications of the ACM. 1969; 12(10):576-580. (In Eng.) DOI: https://doi.org/10.1145/363235.363259
[3] Apt K.R., Olderog E.R. Fifty years of Hoare’s logic. Formal Aspects of Computing. 2019; 31(6):751-807. (In Eng.) DOI: https://doi.org/10.1007/s00165-019-00501-3
[4] Reynolds J.C. Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. Copenhagen, Denmark; 2002. p. 55-74. (In Eng.) DOI: https://doi.org/10.1109/LICS.2002.1029817
[5] Yang H., O’Hearn P. A Semantic Basis for Local Reasoning. In: Nielsen M., Engberg U. (ed.) Foundations of Software Science and Computation Structures. FoSSaCS 2002. Lecture Notes in Computer Science. 2002; 2303:402-416. Springer, Berlin, Heidelberg. (In Eng.) DOI: https://doi.org/10.1007/3-540-45931-6_28
[6] O’Hearn P.W., Pym D.J. The Logic of Bunched Implications. Bulletin of Symbolic Logic. 1999; 5(2):215-244. (In Eng.) DOI: https://doi.org/10.2307/421090
[7] Harel D., Kozen D., Tiuryn J. Dynamic Logic. MIT Press; 2000. Available at: https://mitpress.mit.edu/books/dynamic-logic (accessed 02.09.2020). (In Eng.)
[8] Ahrendt W., Beckert B., Bubel R., et al. Deductive Software Verification – The KeY Book. From Theory to Practice. In: Ahrendt W., et al. Lecture Notes in Computer Science. 2016; 10001. Springer, Cham. (In Eng.) DOI: https://doi.org/10.1007/978-3-319-49812-6
[9] Calcagno C., O'Hearn P.W., Yang H. Local Action and Abstract Separation Logic. In: 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007). Wroclaw, Poland; 2007. p. 366-378. (In Eng.) DOI: https://doi.org/10.1109/LICS.2007.30
[10] Parkinson M., Bornat R., Calcagno C. Variables as Resource in Hoare Logics. In: 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06). Seattle, WA, USA; 2006. p. 137-146. (In Eng.) DOI: https://doi.org/10.1109/LICS.2006.52
[11] Troelstra A., Schwichtenberg H. Basic Proof Theory. 2nd ed., Cambridge Tracts in Theoretical Computer Science. Cambridge, Cambridge University Press; 2000. (In Eng.) DOI: https://doi.org/10.1017/CBO9781139168717
[12] Chlipala A. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press; 2013. Available at: https://mitpress.mit.edu/books/certified-programming-dependent-types (accessed 02.09.2020). (In Eng.)
[13] Chlipala A. Proof engineering: implementation challenges in rigorously verified software. In: Proceedings of the Programming Languages Mentoring Workshop (PLMW '15). Association for Computing Machinery, New York, NY, USA; 2015:8. (In Eng.) DOI: https://doi.org/10.1145/2792434.2792442
[14] Eßmann R., Nipkow T., Robillard S. Verified Approximation Algorithms. In: Peltier N., Sofronie-Stokkermans V. (ed.) Automated Reasoning. IJCAR 2020. Lecture Notes in Computer Science. 2020; 12167:291-306. Springer, Cham. (In Eng.) DOI: https://doi.org/10.1007/978-3-030-51054-1_17
[15] Nipkow T. Term rewriting and beyond - theorem proving in Isabelle. Formal Aspects of Computing. 1989; 1(1):320-338. (In Eng.) DOI: https://doi.org/10.1007/BF01887212
[16] Nipkow T., Klein G. Concrete Semantics: With Isabelle/HOL. Springer, Cham; 2014. (In Eng.) DOI: https://doi.org/10.1007/978-3-319-10542-0
[17] Sergey I., Wilcox J.R., Tatlock Z. Programming and proving with distributed protocols. Proceedings of the ACM on Programming Languages. 2017; 2(POPL):28. (In Eng.) DOI: https://doi.org/10.1145/3158116
[18] Bradley A.R., Manna Z. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Berlin, Heidelberg; 2007. (In Eng.) DOI: https://doi.org/10.1007/978-3-540-74113-8
[19] Filliâtre J.C., Paskevich A. Why3 - Where Programs Meet Provers. In: Felleisen M., Gardner P. (ed.) Programming Languages and Systems. ESOP 2013. Lecture Notes in Computer Science. 2013; 7792:125-128. Springer, Berlin, Heidelberg. (In Eng.) DOI: https://doi.org/10.1007/978-3-642-37036-6_8
[20] Krebbers R., Jung R., Bizjak A., Jourdan J.H., Dreyer D., Birkedal L. The Essence of Higher-Order Concurrent Separation Logic. In: Yang H. (ed.) Programming Languages and Systems. ESOP 2017. Lecture Notes in Computer Science. 2017; 10201:696-723. Springer, Berlin, Heidelberg. (In Eng.) DOI: https://doi.org/10.1007/978-3-662-54434-1_26
[21] Jung R., Jourdan J.-H., Krebbers R., Dreyer D. RustBelt: securing the foundations of the rust programming language. Proceedings of the ACM on Programming Languages. 2017; 2(POPL):66. (In Eng.) DOI: https://doi.org/10.1145/3158154
[22] Brookes S., O’Hearn P.W. Concurrent separation logic. ACM SIGLOG News. 2016; 3(3):47-65. (In Eng.) DOI: https://doi.org/10.1145/2984450.2984457
[23] Xu F., Fu M., Feng X., Zhang X., Zhang H., Li Z. A Practical Verification Framework for Preemptive OS Kernels. In: Chaudhuri S., Farzan A. (ed.) Computer Aided Verification. CAV 2016. Lecture Notes in Computer Science. 2016; 9780:59-79. Springer, Cham. (In Eng.) DOI: https://doi.org/10.1007/978-3-319-41540-6_4
[24] O’Hearn P. Separation Logic. Communications of the ACM. 2019; 62(2):86-95. (In Eng.) DOI: https://doi.org/10.1145/3211968
[25] Zakharova I., Kuzenkov O. The Experience of Updating the Educational Standards of Higher Education in the Field of ICT. Sovremennye informacionnye tehnologii i IT-obrazovanie = Modern Information Technologies and IT-Education. 2017; 13(4):46-57. (In Russ., abstract in Eng.) DOI: https://doi.org/10.25559/SITITO.2017.4.510
[26] Zakharova I., Kuzenkov O. Mathematical Programs Modernization Based on Russian and International Standards. Sovremennye informacionnye tehnologii i IT-obrazovanie = Modern Information Technologies and IT-Education. 2018; 14(1):233-244. (In Eng., abstract in Russ.) DOI: https://doi.org/10.25559/SITITO.14.201801.233-244
[27] Kuzenkov O., Kuzenkova G., Kiseleva T. The use of electronic teaching tools in the modernization of the course “Mathematical modeling of selection processes”. Obrazovatel'nye tehnologii i obshhestvo = Educational Technology & Society. 2018; 21(1):435-448. Available at: https://elibrary.ru/item.asp?id=32253185 (accessed 02.09.2020). (In Russ., abstract in Eng.)
Опубликована
2020-11-30
Как цитировать
MAKAROV, Evgeny Maratovich. Динамическая логика разделений и ее использование в образовании. Международный научный журнал «Современные информационные технологии и ИТ-образование», [S.l.], v. 16, n. 3, p. 543-550, nov. 2020. ISSN 2411-1473. Доступно на: <http://sitito.cs.msu.ru/index.php/SITITO/article/view/696>. Дата доступа: 25 sep. 2021 doi: https://doi.org/10.25559/SITITO.16.202003.543-550.
Раздел
Теоретические вопросы информатики, прикладной математики, компьютерных наук