?
Логика Хоара для императивного языка, учитывающего некоторые аппаратные ограничения
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.