Dynamic Separation Logic and its Use in Education
Abstract
Mathematical logic is widely used in hardware and software verification. Hoare logic is particularly suitable for reasoning about imperative programs. Its extension, separation logic, introduces the separating conjunction, which makes it possible to reason about programs working with pointers and mutable data structures. Dynamic logic, an ex-ample of modal logic, is yet another formalism used for verification. This article introduces propositional dynamic separation logic, which adds separating conjunction to dynamic logic.
We describe syntax, semantics and Hilbert-style deductive system for propositional dynamic separation logic and prove its soundness. The definition of the logic is rather abstract. Thus, the programming language consists of so-called regular programs rather than while-programs, and the set of atomic commands can be arbitrary as long as they correspond to local actions. Special attention is devoted to the soundness of the frame rule, which allows writing program specification using a small footprint, i.e., specifying exactly the portion of the heap that the program reads or writes. Programs that perform tests are also treated differently from regular dynamic logic.
The article also argues for the use of separation logic in computer science curriculum. It is more intuitive that other substructural logics and can be taught even in introductory logic courses. At the same time, it is an active research area with numerous verification tools built on its foundation. Therefore, it serves an excellent introduction to formal methods.
References
[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.)
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publication policy of the journal is based on traditional ethical principles of the Russian scientific periodicals and is built in terms of ethical norms of editors and publishers work stated in Code of Conduct and Best Practice Guidelines for Journal Editors and Code of Conduct for Journal Publishers, developed by the Committee on Publication Ethics (COPE). In the course of publishing editorial board of the journal is led by international rules for copyright protection, statutory regulations of the Russian Federation as well as international standards of publishing.
Authors publishing articles in this journal agree to the following: They retain copyright and grant the journal right of first publication of the work, which is automatically licensed under the Creative Commons Attribution License (CC BY license). Users can use, reuse and build upon the material published in this journal provided that such uses are fully attributed.
