一句话：提出 Outcome Logic，将分支效应置于核心，统一多种带分支效果的程序逻辑并给出相对完备证明系统。
自 Hoare 逻辑以来，人们提出了多种程序逻辑来推理不同类型的程序，但非确定性、概率等导致执行分支的效应往往需要分别处理。本文提出 Outcome Logic，将分支置于核心，用选择的代数表示刻画程序的多结果行为，并系统建立其元理论。作者给出可推理通用循环的相对完备证明系统，证明该系统适用于多种分支效应，能够包容 Hoare 逻辑等已知逻辑，并支持证明片段在不同规约之间的复用。
Starting with Hoare Logic over 50 years ago, numerous program logics have been devised to reason about the different kinds of programs encountered in the real world. This includes reasoning about computational effects, particularly those effects that cause the program execution to branch into multiple paths due to, e.g., nondeterministic or probabilistic choice. Outcome Logic reimagines Hoare Logic with branching at its core, using an algebraic representation of choice to capture programs that branch into many outcomes. In this article, we give a comprehensive account of the Outcome Logic metatheory. This includes a relatively complete proof system for Outcome Logic with the ability to reason about general purpose looping. We also show that this proof system applies to programs with various types of branching, that it subsumes some well-known logics such as Hoare Logic, and that it facilitates the reuse of proof fragments across different kinds of specifications.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Zilberstein25,
title = {Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects},
author = {Noam Zilberstein},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {47},
number = {3},
year = {2025},
doi = {10.1145/3743131}
}