Рамкове правило в монотонному розширенні логіки Флойда – Хоара
Тип публікації :
Стаття
Дата випуску :
5 червня 2026 р.
Автор(и) :
Мова основного тексту :
Англійська
eKNUTSHIR URL :
Том :
82
Випуск :
1
ISSN :
1812-5409
Початкова сторінка :
2218
Кінцева сторінка :
2055
Цитування :
[APA 7] Криволап, А., Шишацька, О., & Русіна, Н. (2026). Frame rule in monotone Floyd – Hoare logic extension. Bulletin of Taras Shevchenko National University of Kyiv. Physics and Mathematics, 82(1), 2218–2055. https://doi.org/10.17721/1812-5409.2026/1.29
[ДСТУ] Криволап А., Шишацька О., Русіна Н. Frame rule in monotone Floyd – Hoare logic extension. Bulletin of Taras Shevchenko National University of Kyiv. Physics and Mathematics. 2026. Vol. 82, no. 1. P. 2218—2055. DOI: 10.17721/1812-5409.2026/1.29 (date of access: 25.07.2026).
Логіка розділення є розширенням логіки Флойда – Хоара, спрямованим на специфікацію та верифікацію програмних систем, в яких використовується динамічна пам’ять. Її основним засобом є рамкове правило, що дає змогу працювати з локальними доведеннями. Монотонне розширення логіки Флойда – Хоара було одержано, використовуючи композиційно-номінативний підхід. Основні переваги отриманої логіки полягають у застосуванні номінативних даних для опису стану програми та у роботі з частковими предикатами. Основна мета пропонованого дослідження – розроблення рамкового правила та засобів роботи з вказівниками для монотонної логіки Флойда – Хоара. З огляду на це, вона була збагачена інструментами для підтримки локальних доведень, що надзвичайно важливо сьогодні, коли складність програмного забезпечення лише зростає. Локальність означає, що властивість частини програми може бути доведена окремо та поєднана з властивостями інших компонентів, якщо визначені умови виконуються. Для цього номінативні дані було розширено поняттям адреси. Представлено нові спеціальні композиції збереження в динамічній пам’яті і завантаження з неї. Логічна зв’язка відокремлювальна кон’юнкція була перевизначена як композиція в програмній алгебрі. Доведено, що така композиція є монотонною. Щоб мати можливість розширити доведення для апроксимацій програми до доведення для програми загалом, усі композиції мають бути монотонними. Крім того, додано правила системи виводу для нових операторів. Правила для зберігання в динамічну пам’ять та завантаження з неї є модифікацією правила для оператора присвоєння. Рамкове правило – це правило, яке за допомогою відокремлювальної кон’юнкції описує, як можна розширити істинну трійку Хоара за допомогою твердження для частини пам’яті, яка не була змінена програмою. Було показано, що варіант правила, реалізований у логіці розділення, вже не є коректним для монотонного розширення. Були представлені модифіковані умови, за яких досягається коректність. Темою майбутніх досліджень є можливі обмеження на операції з вказівниками, які дають можливість запропонувати конструктивні умови для рамкового правила. Іншим важливим питанням, що виходить за межі цієї статті, є розгляд використання складних номінативних даних разом з динамічною пам’яттю.
Файл(и) :![Ескіз]()
Вантажиться...
Формат :
Adobe PDF
Розмір :
253.28 KB
Контрольна сума :
(MD5):172ea55e24795dd814de66f2b1e94559
Якщо не вказано інше, ця робота розповсюджується на умовах ліцензії Creative Commons Attribution 4.0 International