Hoare logic for an imperative language considering some hardware limitations
https://doi.org/10.22405/2226-8383-2025-26-3-113-124
Abstract
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 proofs
conducted 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 contains
an 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 take
hardware 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.
References
1. Winskel G 1993, The Formal Semantics of Programming Languages, The MIT Press, Massachusetts, pp. 11–26. ISBN 0262231697.
2. 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).
3. 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).
4. 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).
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. 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).
6. 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).
7. Voishvillo E K, Degtyarev M G 2001 Logika [Logic]. Vladoss-Press, Moscow, pp. 91–99. ISBN 5-305-00001-7.
8. 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.
Review
For citations:
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
Views:
23
Email this article 