Abstract Hoare Logic has a long tradition in formal verification 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 fibered category theory. We consider Hoare formulas with local, finite 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 fibered one.

Journal Article Towards a uniform presentation of logical systems by indexed categories and adjoint situations Get access U. Wolter, U. Wolter Department of Informatics, University of Bergen, Norway.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar A. Martini, A. Martini Faculdade de Informática, PUCRS, Brasil.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar E. H. Häusler E. H. Häusler Departamento de Ciência da Computação, PUC-Rio, Brasil.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 25, Issue 1, February 2015, Pages 57–93, https://doi.org/10.1093/logcom/exs038 Published: 03 September 2012 Article history Received: 26 January 2012 Published: 03 September 2012