一句话：通过谓词变换器和 TopKAT 建立类 Hoare 逻辑的分类学，并给出 Lisbon 逻辑的新 TopKAT 刻画。
本文研究类 Hoare 逻辑，包括部分正确性与完全正确性 Hoare 逻辑、不正确性逻辑、Lisbon 逻辑等，旨在厘清它们之间的关系。作者从两个统一视角出发：Dijkstra 式谓词变换器，以及带顶与测试的 Kleene 代数（TopKAT）。核心目标是给出这些程序逻辑的分类学，特别关注程序终止、确定性和可逆性等不同假设下逻辑之间的关系如何变化。作为副产品，作者获得了 Lisbon 逻辑的 TopKAT 刻画，据称这是一个新结果。该工作为理解各类 Hoare 式程序逻辑提供了整体视角。
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.
@article{paperbot3237,
title = {A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests},
author = {Lena Verscht and Benjamin Lucien Kaminski},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704896}
}