Indexed and ﬁbered structures for partial and total correctness assertions
Journal article, Peer reviewed
MetadataShow full item record
Original versionMathematical Structures in Computer Science. 2022. 10.1017/S0960129522000275
Hoare Logic has a long tradition in formal veriﬁcation and has been continuously developed and used to verify a broad class of programs, including sequential, object-oriented, and concurrent programs. Here we focus on partial and total correctness assertions within the framework of Hoare logic and show that a comprehensive categorical analysis of its axiomatic semantics needs the languages of indexed and ﬁbered category theory. We consider Hoare formulas with local, ﬁnite contexts, of program and logical variables. The structural features of Hoare assertions are presented in an indexed setting, while the logical features of deduction are modeled in the ﬁbered one.