Frame rule in monotone Floyd – Hoare logic extension
DOI:
https://doi.org/10.17721/1812-5409.2026/1.29Keywords:
formal methods, software verification, program logic, nominative data, separation logicAbstract
Separation logic is an extension of Floyd – Hoare logic, aimed at the specification and verification of programs with a main focus on the representation of dynamic memory handling. Its main tool is the frame rule, which enables local proofs. Applying the composition-nominative approach to classical Floyd – Hoare logic, its monotone extension was developed. The main advantages it offers are the use of nominative data to describe the state of the program and the consideration of partial predicates. The main purpose of this research is to introduce the frame rule and pointer capabilities for monotone Floyd – Hoare logic. This further extension adds support for local reasoning, which is crucial today when the complexity of software only rises. Local reasoning means that a property of a part of the program can be proved separately and combined with proofs for other components if specific conditions hold. For this purpose, the nominative data was enriched with the notion of an address. New special compositions for storing and loading from dynamic memory were introduced. The logical connective separating conjunction was redefined as a composition in program algebra. This composition was proved to be monotone. To extend the proof of the program’s approximations to a complete proof, all compositions have to be monotone. Furthermore, rules for new operators were added to the derivation system. Rules for storing to and loading from dynamic memory are modifications of the rules for the assignment operator. The frame rule states that, with the help of a separating conjunction, a valid Hoare triple can be augmented with an assertion for a part of the memory that was not modified by the program. It was shown that the classic version of the rule, implemented within Separation logic, is not sound for a monotone extension. Conditions for a sound version were presented. Investigation of possible restrictions on the operations with pointers, which will lead to constructive frame rule conditions, is the aim of future research. Complex nominative data with dynamic memory is out of the scope of this paper and should be considered separately.
Pages of the article in the issue: 218 - 224
Language of the article: English
References
Apt, K. R., & Olderog, E.-R. (2019). Fifty years of Hoare’s logic. Formal Aspects of Computing, 31(6), 751–807. https://doi.org/10.1007/s00165-019-00501-3
De Boer, F. S., Hiep, H.-D. A., & de Gouw, S. (2023). Dynamic separation logic. Electronic Notes in Theoretical Informatics and Computer Science, 3, 5:1–5:19. https://doi.org/10.46298/entics.12297
Maksimović, P., Cronjäger, C., Lööw, A., Sutherland, J., & Gardner, P. (2023). Exact separation logic: Towards bridging the gap between verification and bug-finding. In Ali & Salvaneschi (Eds.), 37th European Conference on Object-Oriented Programming (ECOOP 2023) (pp. 19:1–19:27). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.ECOOP.2023.19
Nikitchenko, M., Ivanov, I., Kornilowicz, A., & Kryvolap, A. (2018). Extended Floyd-Hoare logic over relational nominative data. Communications in Computer and Information Science, 826, 41–64. https://doi.org/10.1007/978-3-319-76168-8_3
O’Hearn, P. W. (2019). Incorrectness logic. Proceedings of the ACM on Programming Languages, 4(POPL), 1–32. https://doi.org/10.1145/3371078
O’Hearn, P. W. (2007). Resources, concurrency, and local reasoning. Theoretical Computer Science, 375(1), 271–307. https://doi.org/10.1016/j.tcs.2006.12.035
Raad, A., Berdine, J., Dang, H.-H., Dreyer, D., O’Hearn, P., & Villard, J. (2020). Local reasoning about the presence of bugs: Incorrectness separation logic. In Lahiri & Wang (Eds.), Computer Aided Verification (pp. 225–252). Springer International Publishing. https://doi.org/10.1007/978-3-030-53291-8_14
Reynolds, J. (2002). Separation logic: a logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science (pp. 55–74). IEEE. https://doi.org/10.1109/LICS.2002.1029817
Shkilnyak, S. (2025). Varieties of pure first-order logics of partial quasiary predicates. Bulletin of Taras Shevchenko National University of Kyiv. Physical and Mathematical Sciences, 79(2), 80–88. https://doi.org/10.17721/1812-5409.2024/2.13
Downloads
Published
Issue
Section
License
Copyright (c) 2026 Andrii Kryvolap, Olena Shyshatska, Nataliia Rusina
This work is licensed under a Creative Commons Attribution 4.0 International License.
Authors who publish with this journal agree to the following terms:
- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).
