Total Outcome Logic: Unified Reasoning For Nontermination and Branching Effects
Since their inception in the form of Hoare Logic, program logics have evolvedfar beyond simple imperative programs, expanding to handle memory along- side additional computational effects such as nondeterminism and probabilistic branching. Orthogonally, more recent research has taken a turn toward incor- rectness logics, which prove the presence of bugs rather than their absence, of- fering greater tractability for industrial adoption. However, correctness and incorrectness reasoning have remained funda- mentally incompatible, forcing practitioners to use separate frameworks. This gap was filled by the recently developed Outcome Logic. By decomposing reasoning on the reachability of separate program outcomes, Outcome Logic was able to unify both paradigms as well as generalize across different branch- ing effects. Our work extends Outcome Logic to address one of its blind spots: namely, reasoning about program (non)termination. While specialized logics exist for termination criteria like partial correctness (termination not assured) and total correctness (guaranteed termination), Outcome Logic can only express partial correctness and its dual—guaranteed divergence. In particular, the semantics of Outcome Logic captures only terminating outcomes, precluding reasoning on nonterminating behavior. We expand the syntax, semantics, and proof rules of Outcome Logic to ex- press the full spectrum of termination conditions of programs. As we will see, the mixture of nontermination and nondeterminism requires a nontrivial re- working of the program semantics. Our resulting framework is shown to be sound and relatively complete, as well as expressive enough to subsume re- cently proposed taxonomies of modern program logics. As a proof of concept, we provide case studies demonstrating the ability to perform different kinds of termination analyses in our logic.