Starting with Hoare Logic over 50 years ago, numerous sound and relatively complete 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 effects at its core, using an algebraic representation of choice to capture a variety of effects. In this paper, we give the first relatively complete proof system for Outcome Logic, handling general purpose looping for the first time. We also show that this proof system applies to programs with various effects and that it facilitates the reuse of proof fragments across different kinds of specifications.

翻译：自五十多年前霍耳逻辑问世以来，人们已设计出众多可靠且相对完备的程序逻辑，用于推理现实世界中遇到的各种程序。其中包括对计算效应的推理，特别是那些因非确定性或概率性选择而导致程序执行产生多分支的效应。近期提出的结果逻辑以效应为核心重新构想了霍耳逻辑，利用选择代数的代数表示来捕获多种效应。本文首次给出了结果逻辑的相对完备证明系统，处理了通用循环问题。我们还证明该证明系统适用于具有多种效应的程序，并支持在不同类型的规约间重用证明片段。