A Relatively Complete Program Logic for Effectful Branching

Starting with Hoare Logic over 50 years ago, numerous sound and relativelycomplete program logics have been devised to reason about the diverse programsencountered in the real world. This includes reasoning about computationaleffects, particularly those effects that cause the program execution to branchinto multiple paths due to, e.g., nondeterministic or probabilistic choice. The recently introduced Outcome Logic reimagines Hoare Logic with effects atits core, using an algebraic representation of choice to capture a variety ofeffects. In this paper, we give the first relatively complete proof system forOutcome Logic, handling general purpose looping for the first time. We alsoshow that this proof system applies to programs with various effects and thatit facilitates the reuse of proof fragments across different kinds ofspecifications.