On incorrectness logic and Kleene algebra with top and tests
On incorrectness logic and Kleene algebra with top and tests
复制标题
关于不正确逻辑和带有顶和检验的克林代数
DOI：
10.1145/3498690
复制
发表时间：
2022
影响因子：
--
通讯作者：
Gaboardi, Marco
中科院分区：
文献类型：
--
作者：
Zhang, Cheng;de Amorim, Arthur Azevedo;Gaboardi, Marco
Kleene代数与测试（KAT）是一个用于程序推理的基本方程框架，它在程序转换、网络和编译器优化以及许多其他领域都有应用。在他的开创性工作中，Kozen证明了KAT包含命题Hoare逻辑，表明人们可以利用KAT的等式理论来推理while程序的（部分）正确性。在这项工作中，我们研究了KAT为不正确推理提供的支持，而不是体现在O'Hearn最近提出的不正确逻辑中。我们证明KAT不能直接表达错误逻辑。这种限制的主要原因可以追溯到这样一个事实，即KAT不能显式地表示上域的概念，而上域对于表示不正确三元组是必不可少的。为了解决这个问题，我们研究了带有Top和Tests的Kleene代数（TopKAT），它是带有Top元素的KAT的扩展。我们证明了TopKAT足够强大，可以表示上域运算，表示不正确三元组，并证明了所有不正确逻辑健全的规则。这表明可以利用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.
登录
查看更多内容
使用 Kleene 代数和测试进行编译器优化认证
DOI：
--
发表时间：
2000
期刊：
Computational Logic
影响因子：
--
作者：
D. Kozen;Maria
通讯作者：
Maria
霍尔逻辑和克林代数的检验
DOI：
10.1109/lics.1999.782610
发表时间：
1999
期刊：
Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158)
影响因子：
--
作者：
D. Kozen
通讯作者：
D. Kozen
动态代数和归纳法的本质
DOI：
10.1145/800141.804649
发表时间：
1980
期刊：
Notre Dame J. Formal Log.
影响因子：
--
作者：
V. Pratt
通讯作者：
V. Pratt
领域半环联
DOI：
10.14232/actacyb.291111
发表时间：
2020
期刊：
ArXiv
影响因子：
--
作者：
U. Fahrenberg;Christian Johansen;G. Struth;Krzysztof Ziemi'anksi
通讯作者：
Krzysztof Ziemi'anksi
DOI：
10.1007/978-3-030-53291-8_14
发表时间：
2020-06-16
期刊：
Computer Aided Verification
影响因子：
--
作者：
Raad A;Berdine J;Dang HH;Dreyer D;O’Hearn P;Villard J
通讯作者：
Villard J