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.

翻译：针对缺陷发现的程序逻辑（如近期引入的错误性逻辑）将正确性与错误性视为需要不同逻辑基础的对立概念。本文论证单一统一理论可同时用于正确性与错误性推理。我们提出结果逻辑（Outcome Logic, OL），这是霍尔逻辑的一种新型推广，兼具单子性（以捕获计算效应）与幺半性（以推理结果与可达性）。OL既能表达真正的阳性缺陷，同时保留正确性推理能力。为形式化OL对正确性与错误性的适用性，我们证明任何错误的OL规范均可通过OL自身证伪。我们还利用该框架对非确定性与概率性程序中的新型错误进行推理。基于这些进展，我们主张将OL作为正确性与错误性的新型基础理论。