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