Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
arXiv:2303.03111 · doi:10.1145/3586045
Abstract
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.
References in corpus (5)
Cited by in corpus (9)
- Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
- Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
- Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
- A Demonic Outcome Logic for Randomized Nondeterminism
- Sufficient Incorrectness Logic: SIL and Separation SIL
- Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
- A Complementary Approach to Incorrectness Typing
- Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
- U-Turn: Enhancing Incorrectness Analysis by Reversing Direction