一句话：证明 KAT 无法直接表达不正确性逻辑，并提出 TopKAT 通过顶元素刻画陪域，表达不正确性三元组并证明其规则可靠。
本文研究带测试的 Kleene 代数（KAT）对 O'Hearn 提出的不正确性逻辑的支持能力。作者首先指出 KAT 不能直接表达不正确性逻辑，根本原因是 KAT 无法显式刻画陪域（codomain），而陪域是构造不正确性三元组的关键。为此，作者引入带顶元素和测试的 Kleene 代数（TopKAT），即在 KAT 上增加顶元素。结果显示，TopKAT 足以定义陪域运算、表达不正确性三元组，并证明不正确性逻辑的所有规则可靠。这意味着可以像 Kozen 用 KAT 推理部分正确性那样，用 TopKAT 的等式理论对 while 类程序的不正确性进行推理。
Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT. In this work, we investigate the support that KAT provides for reasoning about incorrectness, instead, as embodied by O'Hearn's recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene Algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of while-like programs by means of the equational theory of TopKAT.
@article{paperbot1599,
title = {On incorrectness logic and Kleene algebra with top and tests},
author = {Cheng Zhang and Arthur Azevedo de Amorim and Marco Gaboardi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498690}
}