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

TL;DR

This work develops a holistic taxonomy of Hoare-like program logics by unifying partial/total correctness and incorrectness logics through predicate transformers and TopKAT. It introduces eight core predicate transformers (wp, wlp, awp, dwp, awlp, dwlp, asp, aslp, along with dsp and dslp) and derives 16 logics by over-/under-approximations, analyzing their interrelations, contrapositions, and equivalences. A novel contribution is expressing Lisbon logic within TopKAT and mapping many logics to TopKAT equations, revealing both symmetries and asymmetries between forward and backward analyses and showing how termination, reachability, determinism, and reversibility collapse or separate logics. The paper also expands the TopKAT perspective, clarifying expressibility limits (e.g., classic total correctness is not in plain KAT) and introducing in-between logics via union/intersection of transformers, with open questions on complexity, proof-rule derivation, and extending algebraic frameworks for divergence. Overall, this integrative approach provides a structured, algebraic lens for comparing, deriving, and potentially mechanizing a broad spectrum of Hoare-like logics that address both correctness and reliability concerns in nondeterministic programs.

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 à 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.

Figures (14)

• Figure 1: Illustration of different coreachability classes and different $\textsf{\upshape {wp}}$ transformers. The top part represents initial states, divided (in columns) into coreachability classes. The lower part represents final states, divided into those that satisfy postcondition $c$ and those that do not. On top, the colored boxed indicate which coreachability classes are included in which transformers.
• Figure 2: Duality of angelic and demonic weakest pre versus angelic and demonic strongest post, demonstrated on four copies of the same program. Preconditions are circled in dashed green, postconditions in dashed blue. The rightmost initial state can terminate in the postcondition, but may also terminate outside. Therefore, it is included in the angelic but not in the demonic weakest precondition. Dually, the leftmost final state is reachable from the precondition but also from outside. Therefore, it is included in the angelic but not in the demonic strongest postcondition.
• Figure 3: An illustration of the different sp-style transformers. The upper part depicts all possible program executions for a fixed final state and a precondition $b$. Below, the colored boxed indicate which sets of final states are included in which transformers.
• Figure 4: Branching divergence versus confluence of unreachability.
• Figure 5: A taxonomy of predicate transformer-based program logics. Black arrows are simple implications, green dotted arrows are contrapositive relations, and orange two-sided arrows are Galois connections.

Theorems & Definitions (36)

• definition 1: Collecting Semantics for $\textnormal{\upshape {nGCL}}\xspace$ Programs
• Remark 1: Diverging Programs
• definition 2: Weakest Precondition Transformers dijkstra1976discipline
• definition 3: Weakest Liberal Precondition Transformers dijkstra1976discipline
• definition 4: Strongest Postcondition Transformer dijkstra1976discipline
• definition 5: Strongest Liberal Postcondition Transformers ZhangKaminski22
• definition 6: Demonic Strongest Postcondition Transformers
• definition 7: Angelic Strongest Liberal Postcondition Transformers
• theorem 1: Ordering on Predicate Transformers
• proof