A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests

TL;DR

This paper provides a comprehensive taxonomy of Hoare-like logics by analyzing their relationships using predicate transformers and Kleene algebras, introducing a novel TopKAT characterization of Lisbon logic.

Contribution

It offers a unified overview of various Hoare-like logics and introduces a new TopKAT-based characterization of Lisbon logic, highlighting their interrelations.

Findings

Unified taxonomy of Hoare-like logics

Novel TopKAT characterization of Lisbon logic

Insights into logic relations under different assumptions

Abstract

We study Hoare-like logics, including partial and total correctness Hoare logic, incorrectness logic, Lisbon logic, and many others through the lens of predicate transformers \`a la Dijkstra and through the lens of Kleene algebra with top and tests (TopKAT). Our main goal is to give an overview - a taxonomy - of how these program logics relate, in particular under different assumptions like for example program termination, determinism, and reversibility. As a byproduct, we obtain a TopKAT characterization of Lisbon logic, which - to the best of our knowledge - is a novel result.