Рамкове правило в монотонному розширенні логіки Флойда – Хоара
DOI:
https://doi.org/10.17721/1812-5409.2026/1.29Ключові слова:
формальні методи, верифікація ПС, програмні логіки, номінативні дані, логіка розділенняАнотація
Логіка розділення є розширенням логіки Флойда – Хоара, спрямованим на специфікацію та верифікацію програмних систем, в яких використовується динамічна пам’ять. Її основним засобом є рамкове правило, що дає змогу працювати з локальними доведеннями. Монотонне розширення логіки Флойда – Хоара було одержано, використовуючи композиційно-номінативний підхід. Основні переваги отриманої логіки полягають у застосуванні номінативних даних для опису стану програми та у роботі з частковими предикатами. Основна мета пропонованого дослідження – розроблення рамкового правила та засобів роботи з вказівниками для монотонної логіки Флойда – Хоара. З огляду на це, вона була збагачена інструментами для підтримки локальних доведень, що надзвичайно важливо сьогодні, коли складність програмного забезпечення лише зростає. Локальність означає, що властивість частини програми може бути доведена окремо та поєднана з властивостями інших компонентів, якщо визначені умови виконуються. Для цього номінативні дані було розширено поняттям адреси. Представлено нові спеціальні композиції збереження в динамічній пам’яті і завантаження з неї. Логічна зв’язка відокремлювальна кон’юнкція була перевизначена як композиція в програмній алгебрі. Доведено, що така композиція є монотонною. Щоб мати можливість розширити доведення для апроксимацій програми до доведення для програми загалом, усі композиції мають бути монотонними. Крім того, додано правила системи виводу для нових операторів. Правила для зберігання в динамічну пам’ять та завантаження з неї є модифікацією правила для оператора присвоєння. Рамкове правило – це правило, яке за допомогою відокремлювальної кон’юнкції описує, як можна розширити істинну трійку Хоара за допомогою твердження для частини пам’яті, яка не була змінена програмою. Було показано, що варіант правила, реалізований у логіці розділення, вже не є коректним для монотонного розширення. Були представлені модифіковані умови, за яких досягається коректність. Темою майбутніх досліджень є можливі обмеження на операції з вказівниками, які дають можливість запропонувати конструктивні умови для рамкового правила. Іншим важливим питанням, що виходить за межі цієї статті, є розгляд використання складних номінативних даних разом з динамічною пам’яттю.
Посилання
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
Завантаження
Опубліковано
Номер
Розділ
Ліцензія
Авторське право (c) 2026 Andrii Kryvolap, Olena Shyshatska, Nataliia Rusina
Ця робота ліцензується відповідно до ліцензії Creative Commons Attribution 4.0 International License.
Автори, роботи яких публікуються у цьому журналі, погоджуються з такими умовами:
- Автори зберігають авторські права та надають журналу право на першу публікацію роботи, яка одночасно ліцензується згідно із Creative Commons Attribution License, тобто надається дозвіл іншим ділитися роботою з визнанням авторства роботи та першої публікації в цьому журналі.
- Автори можуть укладати окремі додаткові угоди щодо невиключного розповсюдження опублікованої журналом версії роботи (наприклад, розмістити її у репозитарії наукової установи чи опублікувати у книзі) з підтвердженням її початкової публікації у цьому журналі.
- Дозволяється та заохочується розміщення своїх робіт в мережі Інтернет авторами (наприклад, у репозитаріях наукових установ або на особистих веб-сторінках) до та під час процесу подання, оскільки це може призвести до продуктивного обміну, а також до більш ранніх цитувань опублікованої роботи та їх більшої кількості (див. The Effect of Open Access).
