Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
复制标题
结果逻辑：正确性和不正确性推理的统一基础
DOI：
--
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Alexandra Silva
中科院分区：
文献类型：
--
作者：
Noam Zilberstein;Derek Dreyer;Alexandra Silva
用于错误查找的程序逻辑（例如最近引入的不正确逻辑）将正确性和不正确性定义为需要不同逻辑基础的双重概念。在本文中，我们认为单一的统一理论既可以用于正确性推理，也可以用于错误性推理。我们提出了结果逻辑（OL），这是霍尔逻辑的一种新颖的概括，它既是单子的（捕获计算效果）又是幺半群的（推理结果和可达性）。 OL 表达真正的积极错误，同时也保留正确性推理能力。为了形式化 OL 对正确性和不正确性的适用性，我们证明任何错误的 OL 规范都可以在 OL 本身中被反驳。我们还使用我们的框架来推理非确定性和概率程序中新型的错误。鉴于这些进展，我们主张将 OL 作为正确与错误的新基础理论。
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory can be used for both correctness and incorrectness reasoning. We present Outcome Logic (OL), a novel generalization of Hoare Logic that is both monadic (to capture computational effects) and monoidal (to reason about outcomes and reachability). OL expresses true positive bugs, while retaining correctness reasoning abilities as well. To formalize the applicability of OL to both correctness and incorrectness, we prove that any false OL specification can be disproven in OL itself. We also use our framework to reason about new types of incorrectness in nondeterministic and probabilistic programs. Given these advances, we advocate for OL as a new foundational theory of correctness and incorrectness.
登录
查看更多内容
DOI：
10.1007/978-3-319-89884-1_5
发表时间：
2018-03
期刊：
ArXiv
影响因子：
--
作者：
G. Barthe;Thomas Espitau;Marco Gaboardi;B. Grégoire;Justin Hsu;Pierre-Yves Strub
通讯作者：
G. Barthe;Thomas Espitau;Marco Gaboardi;B. Grégoire;Justin Hsu;Pierre-Yves Strub
关于不正确逻辑和带有顶和检验的克林代数
影响因子：
--
作者：
Zhang, Cheng;de Amorim, Arthur Azevedo;Gaboardi, Marco
通讯作者：
Gaboardi, Marco
影响因子：
--
作者：
Raad A
通讯作者：
Raad A
通过不正确的逻辑在大型程序中查找真正的错误
影响因子：
--
作者：
Le Q
通讯作者：
Le Q
影响因子：
2.5
作者：
Calcagno, Cristiano;Distefano, Dino;Yang, Hongseok
通讯作者：
Yang, Hongseok