Логика Хоара для императивного языка, учитывающего некоторые аппаратные ограничения
https://doi.org/10.22405/2226-8383-2025-26-3-113-124
Аннотация
В статье определен императивный язык программирования, учитывающий аппаратные ограничения вычислителя с набором инструкций RV32I, заданы его синтаксис и аксиоматическая семантика в виде логики Хоара. Необходимость подобного языка определяется невозможностью напрямую применять формальные доказательства, проведенные для программ на языках, не учитывающих аппаратные ограничения, к транслированному коду, исполняющемуся на реальном аппаратном вычислителе. В то же время проведение доказательств для программ, написанных напрямую в кодах вычислителя, чрезвычайно трудоемко. Описанный язык учитывает такие аппаратные ограничения, как конечная ширина регистра, конечный объем памяти и использование арифметики по модулю вместо классической арифметики. В статье приведен пример программы вычисления НОД двух неотрицательных целых чисел, написанной на этом языке, а также доказательство ее корректности. Таким образом, продемонстрировано, что можно строить формальные доказательства для программ на языке, учитывающем некоторые аппаратные ограничения, и эти доказательства будут сопоставимы по сложности с теми, что построены для аналогичных программ на не учитывающих эти ограничения императивных языках. Одним из направлений развития работы является построение алгоритма трансляции из определенного в статье языка в коды вычислителя и доказательство корректности этого алгоритма.
Об авторе
Даниил Юрьевич Ковалев
Национальный исследовательский университет «Высшая школа экономики»
Россия
Россия
аспирант
Список литературы
1. Winskel G. The Formal Semantics of Programming Languages. The MIT Press, Massachusetts. P. 11–26. ISBN 0262231697.
2. RISC-V Foundation, The RISC-V Instruction Set Manual Volume I Unprivileged Architecture Version 20240411. 2024. URL: https://github.com/riscv/riscv-isa-manual/releases/download/20240411/unpriv-isa-asciidoc.pdf (дата обращения: 23 февраля 2025).
3. RISC-V Foundation, RISC-V ABIs Specification Version 1.0: Ratified. 2022. URL: https://github.com/riscv-non-isa/riscv-elf-psabi-doc/releases/download/v1.0/riscv-abi.pdf (дата обращения: 23 февраля 2025).
4. Hoare C. А. R. An axiomatic basis for computer programming // Communications of the ACM. 1969. vol. 12, issue 10. P. 576–580. doi: 10.1145/363235.363259. URL: https://dl.acm.org/doi/pdf/10.1145/363235.363259 (дата обращения: 23 февраля 2025).
5. Myreen M. O., Gordon M. J. C. Hoare Logic for Realistically Modelled Machine Code // Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2007. Springer-Verlag, Berlin, Heidelberg. P.568–582. doi: 10.1007/978-3-540-71209-1_44. URL: https://link.springer.com/content/pdf/10.1007/978-3-540-71209-1_44.pdf (дата обращения: 23 февраля 2025).
6. McCracken D. D., Reilly E. D. Backus-Naur form (BNF) // In Encyclopedia of Computer Science. 2003. John Wiley and Sons Ltd. P. 129–131. ISBN 0470864125. URL: https://dl.acm.org/doi/pdf/10.5555/1074100.1074155 (дата обращения: 23 февраля 2025).
7. Войшвилло Е. К., Дегтярев М. Г. Логика. 2001. ВЛАДОСС-ПРЕСС, Москва, С. 91–99. ISBN 5-305-00001-7.
8. Jacobs D., Gries D. General correctness: a unification of partial and total correctness // Acta Inf. 1985. vol. 22, num. 1, P. 67–83. doi: 10.1007/BF00290146.
Рецензия
Для цитирования:
Ковалев Д.Ю. Логика Хоара для императивного языка, учитывающего некоторые аппаратные ограничения. Чебышевский сборник. 2025;26(3):113-124. https://doi.org/10.22405/2226-8383-2025-26-3-113-124
For citation:
Kovalev D.Yu. Hoare logic for an imperative language considering some hardware limitations. Chebyshevskii Sbornik. 2025;26(3):113-124. (In Russ.) https://doi.org/10.22405/2226-8383-2025-26-3-113-124
Просмотров:
2
Послать статью по эл. почте 