Starting with Hoare Logic over 50 years ago, numerous program logics have been devised to reason about the diverse 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. The recently introduced 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 expand on prior Outcome Logic papers in order to give a more authoritative and comprehensive account of the 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 and that it facilitates the reuse of proof fragments across different kinds of specifications.

翻译：自50多年前Hoare逻辑问世以来，人们设计了众多程序逻辑来推理现实世界中遇到的各种程序。这包括对计算效应的推理，特别是那些导致程序执行因非确定性或概率性选择等因素而分支为多条路径的效应。最近提出的结果逻辑以分支为核心重新构想了Hoare逻辑，通过选择性的代数表示来捕捉分支为多种结果的程序。本文在先前结果逻辑研究的基础上展开，旨在提供更权威、更全面的元理论阐述。这包括为结果逻辑构建一个相对完备的证明系统，该系统具备推理通用循环结构的能力。我们还证明该证明系统适用于具有多种分支类型的程序，并能促进不同规约间证明片段的重用。