chebЧебышевский сборникChebyshevskii Sbornik2226-8383Tula State Lev Tolstoy Pedagogical University10.22405/2226-8383-2025-26-3-113-124cheb-2009Research ArticleСтатьиArticleЛогика Хоара для императивного языка, учитывающего некоторые аппаратные ограниченияHoare logic for an imperative language considering some hardware limitationsКовалевДаниил ЮрьевичKovalevDaniil Yur’evich

аспирант

postgraduate student

dyukovalev@hse.ruНациональный исследовательский университет «Высшая школа экономики»РоссияHSE UniversityRussian Federation202501112025263113124Copyright © Ковалев Д.Ю., 20252025Ковалев Д.Ю.Kovalev D.Y.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.chebsbornik.ru/jour/article/view/2009

В статье определен императивный язык программирования, учитывающий аппаратные ограничения вычислителя с набором инструкций RV32I, заданы его синтаксис и аксиоматическая семантика в виде логики Хоара. Необходимость подобного языка определяется невозможностью напрямую применять формальные доказательства, проведенные для программ на языках, не учитывающих аппаратные ограничения, к транслированному коду, исполняющемуся на реальном аппаратном вычислителе. В то же время проведение доказательств для программ, написанных напрямую в кодах вычислителя, чрезвычайно трудоемко. Описанный язык учитывает такие аппаратные ограничения, как конечная ширина регистра, конечный объем памяти и использование арифметики по модулю вместо классической арифметики. В статье приведен пример программы вычисления НОД двух неотрицательных целых чисел, написанной на этом языке, а также доказательство ее корректности. Таким образом, продемонстрировано, что можно строить формальные доказательства для программ на языке, учитывающем некоторые аппаратные ограничения, и эти доказательства будут сопоставимы по сложности с теми, что построены для аналогичных программ на не учитывающих эти ограничения императивных языках. Одним из направлений развития работы является построение алгоритма трансляции из определенного в статье языка в коды вычислителя и доказательство корректности этого алгоритма.

In this paper, an imperative programming language considering some hardware limitations of a computer based on the RV32I instruction set is defined, including its syntax and semantics in a form of Hoare logic. The need for such language comes from the fact that formal proofsconducted for programs in languages not considering hardware limitations cannot be directly applied to translated code running on real hardware. At the same time, conducting proofs for programs written directly in machine code is extremely laborious. The language defined in the paper takes into account such hardware limitations as finite register width, finite memory capacity and the usage of modulo arithmetic instead of regular arithmetic. The paper containsan example of a program computing GCD of two non-negative integers, which is written in the proposed language. A proof of the program correctness is also included. Thus, the paper demonstrates that formal proofs could be conducted for programs in the language considering some hardware limitations, and the complexity of the proofs would be comparable to ones conducted for equivalent programs written in regular imperative languages, which do not takehardware limitations into account. Directions for future work include composing an algorithm for translation of the proposed language to machine code and proving the algorithm’s correctness.

логика Хоараформальные методыаксиоматическая семантика.Hoare logicformal methodsaxiomatic semantics.ReferencesWinskel G. The Formal Semantics of Programming Languages. The MIT Press, Massachusetts. P. 11–26. ISBN 0262231697.Winskel G 1993, The Formal Semantics of Programming Languages, The MIT Press, Massachusetts, pp. 11–26. ISBN 0262231697.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).RISC-V Foundation, The RISC-V Instruction Set Manual Volume I Unprivileged Architecture Version 20240411 (2024) Available at: https://github.com/riscv/riscv-isa-manual/releases/download/20240411/unpriv-isa-asciidoc.pdf (accessed 23 February 2025).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).RISC-V Foundation, RISC-V ABIs Specification Version 1.0: Ratified (2022), Available at: https://github.com/riscv-non-isa/riscv-elf-psabi-doc/releases/download/v1.0/riscv-abi.pdf (accessed 23 February 2025).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).Hoare C А R 1969, “An axiomatic basis for computer programming”, Communications of the ACM, vol. 12, issue 10. pp. 576–580. doi: 10.1145/363235.363259. Available at: https://dl.acm.org/doi/pdf/10.1145/363235.363259 (accessed 23 February 2025).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).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. Springer-Verlag, Berlin, Heidelberg, 2007, pp.568–582. doi: 10.1007/978-3-540-71209-1_44. Available at: https://link.springer.com/content/pdf/10.1007/978-3-540-71209-1_44.pdf (accessed 23 February 2025).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).McCracken D D, Reilly E D 2003, “Backus-Naur form (BNF)” In Encyclopedia of Computer Science. John Wiley and Sons Ltd. pp. 129–131. ISBN 0470864125. Available at: https://dl.acm.org/doi/pdf/10.5555/1074100.1074155 (accessed 23 February 2025).Войшвилло Е. К., Дегтярев М. Г. Логика. 2001. ВЛАДОСС-ПРЕСС, Москва, С. 91–99. ISBN 5-305-00001-7.Voishvillo E K, Degtyarev M G 2001 Logika [Logic]. Vladoss-Press, Moscow, pp. 91–99. ISBN 5-305-00001-7.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.Jacobs D, Gries D 1985, “General correctness: a unification of partial and total correctness” Acta Inf., vol. 22, num. 1, pp. 67–83. doi: 10.1007/BF00290146.

The authors declare that there are no conflicts of interest present.