# A Relatively Complete Program Logic for Effectful Branching

Noam Zilberstein<EMAIL_ADDRESS>1234-5678-9012 Cornell UniversityUSA

###### Abstract.

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.

##  1\. Introduction

The seminal work of Floyd (Floyd, 1967a) and Hoare (Hoare, 1969) on program
logics in the 1960s has paved the way towards modern program analysis. The
resulting _Hoare Logic_ —still ubiquitous today—defines triples
${\color[rgb]{.75,0,.25}\\{P\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{Q\\}}$ to
specify the behavior of a program $C$ in terms of a precondition $P$ and a
postcondition $Q$. In the ensuing years, many variants of Hoare Logic have
emerged, in part to handle the numerous computational effects found in real-
world programs.

Such effects include nontermination, arising from while loops; nondeterminism,
useful for modeling opaque aspects of program evaluation such as user input or
concurrent scheduling; and randomization, required for security and machine
learning applications.

These effects have historically warranted specialized program logics with
distinct inference rules. For example, partial correctness (Floyd, 1967a;
Hoare, 1969) vs total correctness (Manna and Pnueli, 1974) can be used to
specify that the postcondition holds _if_ the program terminates vs that it
holds _and_ the programs terminates, respectively. While Hoare Logic has
classically taken a demonic view of nondeterminism (the postcondition must
apply to _all_ possible outcomes), recent work on formal methods for
incorrectness (O’Hearn, 2019; Möller et al., 2021) has motivated the need for
new program logics based on angelic nondeterminism (the postcondition applies
to _some_ reachable outcome). Further, probabilistic Hoare Logics are
quantitative, allowing one to specify the likelihood of each outcome, not just
that they may occur (den Hartog, 2002; Barthe et al., 2018; Rand and
Zdancewic, 2015; den Hartog, 1999).

Despite these apparent differences, all of the aforementioned program logics
share common reasoning principles. For instance, sequences of commands
$C_{1}\fatsemi C_{2}$ are analyzed compositionally and the precondition
(resp., postcondition) can be strengthened (resp., weakened) using logical
consequences, as shown below.

$\inferrule{{\color[rgb]{.75,0,.25}\\{P\\}}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\\{Q\\}}\quad{\color[rgb]{.75,0,.25}\\{Q\\}}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\\{R\\}}}{{\color[rgb]{.75,0,.25}\\{P\\}}~{}C_{1}\fatsemi
C_{2}~{}{\color[rgb]{.75,0,.25}\\{R\\}}}\qquad\inferrule{P^{\prime}\Rightarrow
P\quad{\color[rgb]{.75,0,.25}\\{P\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{Q\\}}\quad
Q\Rightarrow
Q^{\prime}}{{\color[rgb]{.75,0,.25}\\{P^{\prime}\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{Q^{\prime}\\}}}$

As we show in this paper, those common reasoning principles are no mere
coincidence. We give a uniform metatheoretic treatment to program logics with
a variety of computational effects—including nondeterminism and
randomization—culminating in a single relatively complete proof system for all
of them. We also show how specialized reasoning principles (_e.g.,_ loop
invariants for partial correctness) are derived from our more general rules
and how proof fragments can be shared between programs with different effects.

This work is not only of value to theoreticians. Recent interest in static
analysis for incorrectness (O’Hearn, 2019; Raad et al., 2020; Möller et al.,
2021; Le et al., 2022; Raad et al., 2022) has prompted the development of new
program logics, distinct from Hoare Logic. Subsequently—and largely with the
goal of consolidating static analysis tools—more logics were proposed to
capture _both_ correctness (_i.e.,_ Hoare Logic) _and_ incorrectness
(Zilberstein et al., 2023a; Maksimović et al., 2023; Zilberstein et al.,
2023b; Bruni et al., 2021, 2023; Dardinier and Müller, 2023).

One such effort, which we build upon in this paper, is Outcome Logic (OL).
Outcome Logic was first proposed as a unified basis for correctness and
incorrectness reasoning in nondeterministic and probabilistic programs, with
semantics parametric on a _monad_ and a _monoid_ (Zilberstein et al., 2023a).
The semantics was later refined such that each trace is weighted using an
element of a semiring (Zilberstein et al., 2023b). For example, Boolean
weights specify which states are in the set of outcomes for a nondeterministic
program whereas real-valued weights quantify the probabilities of outcomes in
a probabilistic program. Exposing these weights in pre- and postconditions
means that a single program logic can express multiple termination criteria,
angelic _and_ demonic nondeterminism, probabilistic properties, and more.

The previous work on Outcome Logic has investigated its semantics and
connection to separation logic, leaving the proof theory largely unexplored.
Most notably, prior work only supports reasoning about loops via bounded
unrolling, which is not suitable for loops that iterate an indeterminate
number of times. In this paper, we give a full account of the Outcome Logic
proof theory and explore more instances than have been investigated
previously. More precisely, our contributions are as follows:

  * $\triangleright$

We define the Outcome Logic semantics and give five models (Sections 2 and 3),
including a multiset model (Example 2.6) not supported by previous
formalizations due to more restrictive algebraic constraints. Our new looping
construct naturally supports deterministic (while loops), nondeterministic,
and probabilistic iteration—whereas previous OL versions supported fewer kinds
of iteration (Zilberstein et al., 2023b) or used a non-unified, ad-hoc
semantics (Zilberstein et al., 2023a).

  * $\triangleright$

We provide a proof system and prove that it is sound and relatively complete
(Section 4). It is the first OL proof system that handles loops that iterate
an indeterminate number of times. Our Iter rule is sufficient for analyzing
any iterative command, and from it we derive the typical rules for loop
invariants (for partial correctness), loop variants (with termination
guarantees), as well as more complex probabilistic while loops (Section 5).

  * $\triangleright$

We prove that OL subsumes Hoare Logic (Section 3.3) and derive the entire
Hoare Logic proof system (_e.g.,_ loop invariants) in Outcome Logic (Section
5). Inspired by Dynamic Logic (Pratt, 1976), our encoding of Hoare Logic uses
modalities to extend partial correctness beyond just nondeterministic
programs.

  * $\triangleright$

We demonstrate the reusability of proofs across different effects (_e.g.,_
nondeterminism or randomization) and properties (_e.g.,_ angelic or demonic
nondeterminism) (Section 7). Whereas choices about how to handle loops
typically require selecting a specific program logic (_e.g.,_ partial vs total
correctness), loop analysis strategies can be mixed within a single OL
derivation, meaning that static analysis algorithms can avoid recomputing
specifications when analyzing codebases with many procedures.

  * $\triangleright$

We perform combinatorial analysis of graph algorithms based on alternative
computation models (Section 8).

  * $\triangleright$

We contextualize the paper in terms of related work and discuss the outlooks
(Section 9).

##  2\. Weighted Program Semantics

We begin the technical development by defining a basic programming language
and describing its semantics based on various interpretations of choice. The
syntax for the language is shown below.

$\displaystyle C$ $\displaystyle\Coloneqq\mathsf{skip}\mid C_{1}\fatsemi
C_{2}\mid C_{1}+C_{2}\mid\mathsf{assume}~{}e\mid{C}^{\langle
e,e^{\prime}\rangle}\mid a\in\mathsf{Act}$ $\displaystyle e$
$\displaystyle\Coloneqq b\mid u\in U$ $\displaystyle b$
$\displaystyle\Coloneqq\mathsf{true}\mid\mathsf{false}\mid b_{1}\lor b_{2}\mid
b_{1}\land b_{2}\mid\lnot b\mid t\in\mathsf{Test}$

At first glance, this language appears similar to imperative languages such as
Dijkstra’s Guarded Command Language (GCL) (Dijkstra, 1975), with familiar
constructs such as $\mathsf{skip}$, sequential composition ($C_{1}\fatsemi
C_{2}$), choice ($C_{1}+C_{2}$), and primitive actions $a\in\mathsf{Act}$. The
differences arise from the generalized $\mathsf{assume}$ operation, which
weights the current computation branch using an expression $e$ (either a test
$b$ or a _weight_ $u\in U$, which will be described in Section 2.1).

Weighting is also used in the iteration command ${C}^{\langle
e,e^{\prime}\rangle}$, which iterates $C$ with weight $e$ and exits with
weight $e^{\prime}$. It is a generalization of the Kleene star $C^{\star}$,
and is also more general than the iteration constructs found in previous
Outcome Logic work (Zilberstein et al., 2023a, b). In Section 2.3, we will
show how to encode while loops, Kleene star, and probabilistic loops using
${C}^{\langle e,e^{\prime}\rangle}$. Although the latter constructs can be
encoded using while loops and auxiliary variables, capturing this behavior
_without_ state opens up the possibility for complete equational theories over
uninterpreted atomic commands (Kozen, 1997; Różowski et al., 2023).

Tests $b$ contain the typical operations of Boolean algebras as well as
primitive tests $t\in\mathsf{Test}$, assertions about a program state.
Primitive tests are represented semantically, so
$\mathsf{Test}\subseteq\dsser{2}^{\Sigma}$ where $\Sigma$ is the set of
program states (each primitive test $t\subseteq\Sigma$ is the set of states
that it describes). Tests evaluate to $\dsser{0}$ or $\dsser{1}$, which are
abstract Booleans representing false and true, respectively.

The values $\dsser{0}$ and $\dsser{1}$ are two examples of weights from the
set $\\{\dsser{0},\dsser{1}\\}\subseteq U$. These weights have particular
algebraic properties that will be described fully in Section 2.1. The command
$\mathsf{assume}~{}b$ can be thought of as choosing whether or not to continue
evaluating the current branch of computation, whereas $\mathsf{assume}~{}u$
more generally picks a weight for the branch, which may be a Boolean
($\dsser{0}$ or $\dsser{1}$), but may also be some other type of weight such
as a probability. In the remainder of this section, we will define the
semantics formally.

###  2.1. Algebraic Preliminaries

We begin by reviewing some algebraic structures. First, we define the
properties of the weights for each computation branch.

###### Definition 2.1 (Monoid).

A monoid $\langle U,+,\dsser{0}\rangle$ consists of a carrier set $U$, an
associative binary operation $+\colon U\times U\to U$, and an identity element
$\dsser{0}\in U$ ($u+\dsser{0}=\dsser{0}+u=u$). If $+\colon U\times
U\rightharpoonup U$ is partial, then the monoid is partial. If $+$ is
commutative ($u+v=v+u$), then the monoid is commutative.

As an example, $\langle\\{0,1\\},\lor,0\rangle$ is a monoid on Booleans.

###### Definition 2.2 (Semiring).

A semiring $\langle U,+,\cdot,\dsser{0},\dsser{1}\rangle$ is an algebraic
structure such that $\langle U,+,\dsser{0}\rangle$ is a commutative monoid,
$\langle U,\cdot,\dsser{1}\rangle$ is a monoid, and the following additional
properties hold:

  1. (1)

Distributivity: $u\cdot(v+w)=u\cdot v+u\cdot w$ and $(u+v)\cdot w=u\cdot
w+v\cdot w$

  2. (2)

Annihilation: $\dsser{0}\cdot u=u\cdot\dsser{0}=\dsser{0}$

The semiring is partial if $\langle U,+,\dsser{0}\rangle$ is a partial monoid
(but $\cdot$ is total).

Semirings elements will act as the _weights_ for traces in our semantics. That
is, the interpretation of a program at a state $\sigma\in\Sigma$ will map each
end state to a semiring element $\left\llbracket
C\right\rrbracket(\sigma)\colon\Sigma\to U$. Varying the semiring will give us
different kinds of effects. For example, a Boolean semiring where
$U=\\{0,1\\}$ corresponds to nondeterministic computation; $\left\llbracket
C\right\rrbracket(\sigma)\colon\Sigma\to\\{0,1\\}\cong\dsser{2}^{\Sigma}$
tells us which states are in the set of nondeterministic outcomes. A
probabilistic semiring where $U=[0,1]$ (the unit interval of real numbers)
gives us a map from states to probabilities—a _distribution_ of outcomes. More
formally, the result is a _weighting function_ , defined below.

###### Definition 2.3 (Weighting Function).

Given a set $X$ and a partial semiring $\mathcal{A}=\langle
U,+,\cdot,\dsser{0},\dsser{1}\rangle$, the set of weighting functions is:

$\mathcal{W}_{\mathcal{A}}(X)\triangleq\Big{\\{}m\colon X\to
U~{}\Big{|}~{}|m|~{}\text{is defined and}~{}\mathsf{supp}(m)~{}\text{is
countable}\Big{\\}}$

Where $\mathsf{supp}(m)\triangleq\\{\sigma\mid m(\sigma)\neq\dsser{0}\\}$,
$|m|\triangleq{\sum_{\sigma\in\mathsf{supp}(m)}}m(\sigma)$, and $\sum$ is an
operation based on $+$ described in Appendix A.

Weighting functions can encode the following types of computation.

###### Example 2.4 (Nondeterminism).

Nondeterministic computation is based on the Boolean semiring
$\mathsf{Bool}=\langle\mathbb{B},\vee,\wedge,0,1\rangle$, where weights are
drawn from $\mathbb{B}=\\{0,1\\}$ and _conjunction_ $\land$ and _disjunction_
$\lor$ are the usual logical operations. This gives us
$\mathcal{W}_{\mathsf{Bool}}(X)\cong\dsser{2}^{X}$—weighting functions on
$\mathsf{Bool}$ are isomorphic to sets.

###### Example 2.5 (Determinism).

Deterministic computation also uses Boolean weights, but with a different
interpretation of the semiring $+$; that is, $0+x=x+0=x$, but $1+1$ is
undefined. The semiring is therefore
$\mathsf{Bool}^{\prime}=\langle\mathbb{B},+,\land,0,1\rangle$. With this
definition of $+$, the requirement of Definition 2.3 that $|m|$ is defined
means that $|\mathsf{supp}(m)|\leq 1$, so we get that
$\mathcal{W}_{\mathsf{Bool}^{\prime}}(X)\cong X+1$—it is either a single value
$x\in X$, or $\star\in 1$, indicating that the program diverged.

###### Example 2.6 (Multiset Nondeterminism).

Rather than indicating which outcomes are possible using Booleans, we use
natural numbers (extended with $\infty$) $n\in\mathbb{N}^{\infty}$ to count
the traces leading to each outcome. This gives us the semiring
$\mathsf{Nat}=\langle\mathbb{N}^{\infty},+,\cdot,0,1\rangle$ where $+$ and
$\cdot$ are the standard arithmetic operations, and we get that
$\mathcal{W}_{\mathsf{Nat}}(X)\cong\mathcal{M}(X)$ where $\mathcal{M}(X)$ is a
_multiset_.

###### Example 2.7 (Randomization).

Probabilities $p\in[0,1]\subset\mathbb{R}$ form a partial semiring
$\mathsf{Prob}=\langle[0,1],+,\cdot,0,1\rangle$ where $+$ and $\cdot$ are
real-valued arithmetic operations, but $+$ is undefined if $x+y>1$ (just like
in Example 2.5). This gives us
$\mathcal{W}_{\mathsf{Prob}}(X)\cong\mathcal{D}(X)$, where $\mathcal{D}(X)$ is
a probability sub-distribution (meaning that the mass can be less than 1 if
some traces diverge).

###### Example 2.8 (Tropical Computation).

The tropical semiring
$\mathsf{Tropical}=\langle[0,\infty],\min,+,\infty,0\rangle$ uses real-valued
weights, but $+$ is minimum and $\cdot$ is addition. Computations in
$\mathcal{W}_{\mathsf{Tropical}}(X)$ therefore correspond to programs that
choose the _cheapest_ path for each outcome.

We will occasionally write $\mathcal{W}(X)$ instead of
$\mathcal{W}_{\mathcal{A}}(X)$ when $\mathcal{A}$ is obvious. The semiring
operations for addition, scalar multiplication, and zero are lifted pointwise
to weighting functions as follows

$(m_{1}+m_{2})(x)\triangleq m_{1}(x)+m_{2}(x)\quad(u\cdot m)(x)\triangleq
u\cdot m(x)\quad\dsser{0}(x)\triangleq\dsser{0}$

These lifted semiring operations give us a way to interpret branching, but we
also need an interpretation for sequential composition. As is standard in
program semantics with effects, we use a monad, which we define as a Klesli
triple (Manes, 1976; Moggi, 1991).

###### Definition 2.9 (Kleisli Triple).

A Kleisli triple $\langle T,\eta,(-)^{\dagger}\rangle$ in $\mathbf{Set}$
consists of a functor $T\colon\mathbf{Set}\to\mathbf{Set}$, and two morphisms
$\eta:\mathsf{Id}\Rightarrow T$ and $(-)^{\dagger}\colon(X\to T(Y))\to T(X)\to
T(Y)$ such that:

$\eta^{\dagger}=\mathsf{id}\qquad f^{\dagger}\circ\eta=f\qquad
f^{\dagger}\circ g^{\dagger}=(f^{\dagger}\circ g)^{\dagger}$

For any semiring $\mathcal{A}$,
$\langle\mathcal{W}_{\mathcal{A}},\eta,(-)^{\dagger}\rangle$ is a Kleisli
triple where the operations $\eta$ and $(-)^{\dagger}$ are defined below.

$\eta(x)(y)\triangleq\left\\{\begin{array}[]{lll}\dsser{1}&\text{if}&x=y\\\
\dsser{0}&\text{if}&x\neq y\end{array}\right.\qquad
f^{\dagger}(m)(y)\triangleq\smashoperator[]{\sum_{x\in\mathsf{supp}(m)}^{}}m(x)\cdot
f(x)(y)$

###  2.2. Denotational Semantics

We interpret the semantics of our language using the five-tuple
$\langle\mathcal{A},\Sigma,\mathsf{Act},\mathsf{Test},\left\llbracket\cdot\right\rrbracket_{\mathsf{Act}}\rangle$,
where the components are:

  1. (1)

$\mathcal{A}=\langle U,+,\cdot,\dsser{0},\dsser{1}\rangle$ is a naturally
ordered, complete, Scott continuous111These concepts are defined formally in
Appendix A., partial semiring with a top element $\top\in U$ such that
$\top\geq u$ for all $u\in U$.

  2. (2)

$\Sigma$ is the set of concrete program states.

  3. (3)

$\mathsf{Act}$ is the set of atomic actions.

  4. (4)

$\mathsf{Test}\subseteq\dsser{2}^{\Sigma}$ is the set of primitive tests.

  5. (5)

$\left\llbracket-\right\rrbracket_{\mathsf{Act}}\colon\mathsf{Act}\to\Sigma\to\mathcal{W}_{\mathcal{A}}(\Sigma)$
is the semantic interpretation of atomic actions.

This definition is a generalized version of the one used in Outcome Separation
Logic (Zilberstein et al., 2023b). For example, we have dropped the
requirement that $\top=\dsser{1}$, meaning that we can capture more types of
computation, such as the multiset model (Example 2.6).

Commands are interpreted as maps from states $\sigma\in\Sigma$ to weighting
functions on states $\left\llbracket
C\right\rrbracket\colon\Sigma\to\mathcal{W}_{\mathcal{A}}(\Sigma)$, as shown
in Figure 1. The first three commands are defined in terms of the monad and
semiring operations (Definitions 2.3 and 2.2): $\mathsf{skip}$ uses $\eta$,
sequential composition $C_{1}\fatsemi C_{2}$ uses $(-)^{\dagger}$, and
$C_{1}+C_{2}$ uses the (lifted) semiring $+$. Since $+$ is partial, the
semantics of $C_{1}+C_{2}$ may be undefined. In Section 2.3, we discuss simple
syntactic checks to ensure that the semantics is total. Atomic actions are
interpreted using $\left\llbracket\cdot\right\rrbracket_{\mathsf{Act}}$.

$\displaystyle\left\llbracket\mathsf{skip}\right\rrbracket(\sigma)$
$\displaystyle\triangleq\eta(\sigma)$ $\displaystyle\left\llbracket
C_{1}\fatsemi C_{2}\right\rrbracket(\sigma)$
$\displaystyle\triangleq\left\llbracket
C_{2}\right\rrbracket^{\dagger}\\!(\left\llbracket
C_{1}\right\rrbracket(\sigma))$ $\displaystyle\left\llbracket
C_{1}+C_{2}\right\rrbracket(\sigma)$ $\displaystyle\triangleq\left\llbracket
C_{1}\right\rrbracket(\sigma)+\left\llbracket C_{2}\right\rrbracket(\sigma)$
$\displaystyle\left\llbracket a\right\rrbracket(\sigma)$
$\displaystyle\triangleq\left\llbracket
a\right\rrbracket_{\mathsf{Act}}(\sigma)$
$\displaystyle\left\llbracket\mathsf{assume}~{}e\right\rrbracket(\sigma)$
$\displaystyle\triangleq\left\llbracket
e\right\rrbracket(\sigma)\cdot\eta(\sigma)$
$\displaystyle\left\llbracket{C}^{\langle
e,e^{\prime}\rangle}\right\rrbracket(\sigma)$
$\displaystyle\triangleq\Big{(}\mu f.\Phi_{\langle
C,e,e^{\prime}\rangle}(f)\Big{)}(\sigma)$ where $\displaystyle\Phi_{\langle
C,e,e^{\prime}\rangle}(f)(\sigma)$ $\displaystyle=\left\llbracket
e\right\rrbracket(\sigma)\cdot f^{\dagger}(\left\llbracket
C\right\rrbracket(\sigma))+\left\llbracket
e^{\prime}\right\rrbracket(\sigma)\cdot\eta(\sigma)$ Figure 1. Denotational
semantics for commands $\left\llbracket
C\right\rrbracket\colon\Sigma\rightharpoonup\mathcal{W}_{\mathcal{A}}(\Sigma)$,
given a partial semiring $\mathcal{A}=\langle
X,+,\cdot,\dsser{0},\dsser{1}\rangle$, a set of program states $\Sigma$,
atomic actions $\mathsf{Act}$, primitive tests $\mathsf{Test}$, and an
interpretation of atomic actions $\left\llbracket
a\right\rrbracket_{\mathsf{Act}}\colon\Sigma\to\mathcal{W}_{\mathcal{A}}(\Sigma)$.

The interpretation of $\mathsf{assume}$ relies on the ability to interpret
expressions and tests. We first describe the interpretation of tests, which
maps tests $b$ to the weights $\dsser{0}$ or $\dsser{1}$, that is
$\left\llbracket
b\right\rrbracket_{\mathsf{Test}}\colon\Sigma\to\\{\dsser{0},\dsser{1}\\}$,
with $\dsser{0}$ representing false and $\dsser{1}$ representing true, so
$\left\llbracket\mathsf{false}\right\rrbracket(\sigma)=\dsser{0}$ and
$\left\llbracket\mathsf{true}\right\rrbracket(\sigma)=\dsser{1}$. The
operators $\land$, $\lor$, and $\lnot$ are interpreted in the obvious ways,
and for primitive tests $\left\llbracket t\right\rrbracket(\sigma)=\dsser{1}$
if $\sigma\in t$ otherwise $\left\llbracket
t\right\rrbracket(\sigma)=\dsser{0}$. The full semantics of tests is given in
Section A.1.

Since an expression is either a test or a weight, it remains only to describe
the interpretation of weights, which is $\left\llbracket
u\right\rrbracket(\sigma)=u$ for any $u\in U$. So, $\mathsf{assume}~{}e$ uses
$\left\llbracket e\right\rrbracket\colon\Sigma\to U$ to obtain a program
weight, and then scales the current state by it. If a test evaluates to false,
then the weight of the branch is $\dsser{0}$, so it is eliminated. If it
evaluates to true, then the weight is scaled by $\dsser{1}$—the identity of
multiplication—so the weight is unchanged.

The iteration command continues with weight $e$ and terminates with weight
$e^{\prime}$. We can attempt to define it recursively as follows.

$\displaystyle\left\llbracket{C}^{\langle
e,e^{\prime}\rangle}\right\rrbracket(\sigma)$
$\displaystyle=\left\llbracket\mathsf{assume}~{}e\fatsemi
C\fatsemi{C}^{\langle
e,e^{\prime}\rangle}+\mathsf{assume}~{}e^{\prime}\right\rrbracket(\sigma)$
$\displaystyle=\left\llbracket
e\right\rrbracket(\sigma)\cdot\left\llbracket{C}^{\langle
e,e^{\prime}\rangle}\right\rrbracket^{\dagger}\\!(\left\llbracket
C\right\rrbracket(\sigma))+\left\llbracket
e^{\prime}\right\rrbracket(\sigma)\cdot\eta(\sigma)$

In reality, we define the loop semantics as a least fixed point (denoted by
the $\mu$ operator). Some additional requirements on the partial semiring
(completeness and Scott continuity) ensure that this fixed point exists. For
the full details, see Appendix A.

###  2.3. Syntactic Sugar for Total Programs

As mentioned in the previous section, the semantics of $C_{1}+C_{2}$ and
${C}^{\langle e,e^{\prime}\rangle}$ are not always defined given the
partiality of the semiring $+$. The ways that $+$ can be used in programs
depends on the particular semiring. However, regardless of the semiring,
guarded choice (_i.e.,_ if statements) are always valid, which we define as
syntactic sugar.

$\mathsf{if}~{}b~{}\mathsf{then}~{}C_{1}~{}\mathsf{else}~{}C_{2}\triangleq(\mathsf{assume}~{}b\fatsemi
C_{1})+(\mathsf{assume}~{}\lnot b\fatsemi C_{2})$

Since $\mathsf{Bool}$, $\mathsf{Nat}$, and $\mathsf{Tropical}$ are total
semirings, unguarded choice is always valid in those execution models. In the
probabilistic case, choice can be used as long as the sum of the weights of
both branches is at most 1. One way to achieve this is to weight one branch by
a probability $p\in[0,1]$ and the other branch by $1-p$, a biased coin-flip.
We provide syntactic sugar for that operation:

$C_{1}+_{p}C_{2}\triangleq(\mathsf{assume}~{}p\fatsemi
C_{1})+(\mathsf{assume}~{}1-p\fatsemi C_{2})$

We also provide syntactic sugar for iterating constructs below.

$\mathsf{while}~{}b~{}\mathsf{do}~{}C\triangleq{C}^{\langle b,\lnot
b\rangle}\qquad
C^{\star}\triangleq{C}^{\langle\dsser{1},\dsser{1}\rangle}\qquad C^{\langle
p\rangle}\triangleq{C}^{\langle p,1-p\rangle}$

While loops use a test to determine whether iteration should continue, making
them deterministic. The Kleene star $C^{\star}$ is defined for interpretations
based on total semirings only; it iterates $C$ nondeterministically many
times.222 In nondeterministic languages,
$\mathsf{while}~{}b~{}\mathsf{do}~{}C\equiv(\mathsf{assume}~{}b\fatsemi
C)^{\star}\fatsemi\mathsf{assume}~{}\lnot b$, however this encoding does not
work in general since $(\mathsf{assume}~{}b\fatsemi C)^{\star}$ is not a well-
defined program when using a partial semiring (_e.g.,_ Examples 2.5 and 2.7).

Finally, the probabilistic iterator $C^{\langle p\rangle}$ continues to
execute with probability $p$ and exits with probability $1-p$. This behavior
can be replicated using a while loop and auxiliary variables, but adding state
complicates reasoning about the programs and precludes, _e.g.,_ devising
equational theories over uninterpreted atomic commands (Różowski et al.,
2023). This construct—which was not included in previous Outcome Logic work—is
therefore advantageous.

In Appendix A, we prove that programs constructed using appropriate syntax
have total semantics. For the remainder of the paper, we assume that programs
are constructed in this way, and are thus always well-defined.

##  3\. Outcome Logic

In this section, we define Outcome Logic, and show how it relates to Hoare
Logic and Dynamic Logic (Pratt, 1976).

###  3.1. Outcome Assertions

Outcome assertions are the basis for expressing pre- and postconditions in
Outcome Logic. Unlike pre- and postconditions of Hoare Logic—which can only
describe _individual program states_ —outcome assertions expose the program
weights from Section 2.1 to enable reasoning about branching and the weights
of reachable outcomes.

We represent these assertions semantically; outcome assertions
$\varphi,\psi\in\dsser{2}^{\mathcal{W}_{\mathcal{A}}(\Sigma)}$ are the sets of
weighted collections of program states representing their true assignments.
For any $m\in\mathcal{W}_{\mathcal{A}}(\Sigma)$, we write $m\vDash\varphi$
($m$ satisfies $\varphi$) to mean that $m\in\varphi$.

The use of semantic assertions allows us to focus on the rules of inference
pertaining to the structure of programs, showing that the proof system is
sufficient for all practical purposes. No program logic is truly complete, as
analyzing loops inevitably reduces to the (undecidable) halting problem (Apt,
1981; Cook, 1978). It is well known that in order to express intermediate
assertions and loop invariants, the assertion language must at least contain
Peano arithmetic (Lipton, 1977), making the details of this language somewhat
uninteresting. As a result, many modern developments such as Separation Logic
(Calcagno et al., 2007; Yang, 2001), Incorrectness Logic (O’Hearn, 2019), Iris
(Jung et al., 2015, 2018), probabilistic Hoare-style logics (Barthe et al.,
2018; Kaminski, 2019), and others (Dardinier and Müller, 2023; Raad et al.,
2023; Cousot et al., 2012; Ascari et al., 2023) use semantic assertions.

$\displaystyle\top$ $\displaystyle\triangleq\mathcal{W}_{\mathcal{A}}(\Sigma)$
$\displaystyle\lnot\varphi$
$\displaystyle\triangleq\mathcal{W}_{\mathcal{A}}(\Sigma)\setminus\varphi$
$\displaystyle\bot$ $\displaystyle\triangleq\emptyset$
$\displaystyle\varphi\Rightarrow\psi$
$\displaystyle\triangleq(\mathcal{W}_{\mathcal{A}}(\Sigma)\setminus\varphi)\cup\psi$
$\displaystyle\varphi\vee\psi$ $\displaystyle\triangleq\varphi\cup\psi$
$\displaystyle\mathbf{1}_{m}$ $\displaystyle\triangleq\\{m\\}$
$\displaystyle\varphi\land\psi$ $\displaystyle\triangleq\varphi\cap\psi$
$\displaystyle\exists x:T.\phi(x)$ $\displaystyle\triangleq\bigcup_{t\in
T}\phi(t)$

$\displaystyle\varphi\oplus\psi$ $\displaystyle\triangleq\\{m_{1}+m_{2}\mid
m_{1}\in\varphi,m_{2}\in\psi\\}$ $\displaystyle\varphi^{(u)}$
$\displaystyle\triangleq\\{u\cdot m\mid m\in\varphi\\}\cup\\{\dsser{0}\mid
u=\dsser{0}\\}$
$\displaystyle{{\vphantom{P}}^{\ulcorner}\kern-0.5pt\mspace{0.0mu}{{}P}^{\urcorner}}$
$\displaystyle\triangleq\\{m\in\mathcal{W}_{\mathcal{A}}(\Sigma)\mid|m|=\dsser{1},\mathsf{supp}(m)\subseteq
P\\}$

Figure 2. Outcome assertion semantics, given a partial semiring
$\mathcal{A}=\langle U,+,\cdot,\dsser{0},\dsser{1}\rangle$ where $u\in U$,
$\phi\colon T\to\dsser{2}^{\mathcal{W}_{\mathcal{A}}(\Sigma)}$, and
$P\in\dsser{2}^{\Sigma}$.

We will now define useful notation for common assertions, which are also
repeated in Figure 2. For example $\top$ (always true) is the set of all
weighted collections, $\bot$ (always false) is the empty set, and logical
negation is the set complement.

$\top\triangleq\mathcal{W}_{\mathcal{A}}(\Sigma)\qquad\quad\bot\triangleq\emptyset\qquad\quad\lnot\varphi\triangleq\mathcal{W}_{\mathcal{A}}(\Sigma)\setminus\varphi$

Disjunction, conjunction, and implication are defined as usual:

$\varphi\lor\psi\triangleq\varphi\cup\psi\qquad\varphi\land\psi\triangleq\varphi\cap\psi\qquad\varphi\Rightarrow\psi\triangleq(\mathcal{W}_{\mathcal{A}}(\Sigma)\setminus\varphi)\cup\psi$

Given a predicate $\phi\colon
T\to\dsser{2}^{\mathcal{W}_{\mathcal{A}}(\Sigma)}$ on some (possibly infinite)
set $T$, existential quantification over $T$ is the union of $\phi(t)$ for all
$t\in T$, meaning it is true iff there is some $t\in T$ that makes $\phi(t)$
true.

$\exists x:T.~{}\phi(x)\triangleq\bigcup_{t\in T}\phi(t)$

Next, we define assertions based on the operations of the semiring
$\mathcal{A}=\langle U,+,\cdot,\dsser{0},\dsser{1}\rangle$. The _outcome
conjunction_ $\varphi\oplus\psi$ asserts that the collection of outcomes $m$
can be split into two parts $m=m_{1}+m_{2}$ such that $\varphi$ holds in
$m_{1}$ and $\psi$ holds in $m_{2}$333 We remark that $\oplus$ is semantically
equivalent to the separating conjunction ($\ast$) from the logic of Bunched
Implications (BI) (O’Hearn and Pym, 1999), but a deeper exploration is out of
scope. .

$\varphi\oplus\psi\triangleq\\{m_{1}+m_{2}\mid
m_{1}\in\varphi,m_{2}\in\psi\\}$

For example, in the nondeterministic interpretation, we can view $m_{1}$ and
$m_{2}$ as sets (not necessarily disjoint), such that $m=m_{1}\cup m_{2}$, so
$\varphi$ and $\psi$ each describe subsets of the reachable states.

The weighting operation $\varphi^{(u)}$ means that $\varphi$ occurs with
weight $u$, where $u\in U$ is a literal weight. We also ensure that
$\dsser{0}\in\varphi^{(\dsser{0})}$ so that
$\varphi\oplus\psi^{(\dsser{0})}\Leftrightarrow\varphi$ even if $\psi$ is
unsatisfiable.

$\varphi^{(u)}\triangleq\\{u\cdot m\mid m\in\varphi\\}\cup\\{\dsser{0}\mid
u=\dsser{0}\\}$

Finally, we provide a way to lift atomic assertions $P\subseteq\Sigma$
describing some subset of the program states. When lifted to be an outcome
assertion,
${{\vphantom{P}}^{\ulcorner}\kern-0.5pt\mspace{0.0mu}{{}P}^{\urcorner}}$ must
cover all the reachable states ($\mathsf{supp}(m)\subseteq P$). We also
require that $|m|=\dsser{1}$. In the nondeterministic case (Example 2.4), this
simply means that $m\neq\emptyset$, and so $P$ is non-vacuously satisfied. In
the probabilistic case (Example 2.7), this means that the probability of $P$
occurring is exactly 1. It also means that in
${{\vphantom{P}}^{\ulcorner}\kern-0.5pt\mspace{0.0mu}{{}P}^{\urcorner}}^{(p)}$,
the probability of $P$ occurring is exactly $p$ and that
$\eta(\sigma)\vDash{{\vphantom{P}}^{\ulcorner}\kern-0.5pt\mspace{0.0mu}{{}P}^{\urcorner}}$
for any $\sigma\in P$.

${{\vphantom{P}}^{\ulcorner}\kern-0.5pt\mspace{0.0mu}{{}P}^{\urcorner}}\triangleq\\{m\mid|m|=\dsser{1},\mathsf{supp}(m)\subseteq
P\\}$

We will often omit the lifting brackets
${{\vphantom{-}}^{\ulcorner}\kern-0.5pt\mspace{0.0mu}{{}-}^{\urcorner}}$ and
simply write ${\color[rgb]{.75,0,.25}\langle
P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle Q\rangle}$. We also permit the
use of tests $b$ in triples. For instance, the precondition of
${\color[rgb]{.75,0,.25}\langle P\land
b\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle Q\rangle}$ is the set:

$\\{m\in\mathcal{W}(\Sigma)\mid|m|=\dsser{1},\forall\sigma\in\mathsf{supp}(m).~{}\sigma\in
P\land\left\llbracket b\right\rrbracket_{\mathsf{Test}}(\sigma)=\dsser{1}\\}$

There is a close connection between the $\oplus$ of outcome assertions and the
choice operator $C_{1}+C_{2}$ for programs. If $P$ is an assertion describing
the outcome of $C_{1}$ and $Q$ describes the outcome of $C_{2}$, then $P\oplus
Q$ describes the outcome of $C_{1}+C_{2}$ by stating that both $P$ and $Q$ are
reachable outcomes via a non-vacuous program trace. This is more expressive
than using the disjunction $P\vee Q$, since the disjunction does not guarantee
that _both_ $P$ and $Q$ are reachable. Suppose $P$ describes a desirable
program outcome whereas $Q$ describes an erroneous one; then $P\oplus Q$ tells
us that the program has a bug (it can reach an error state) whereas $P\vee Q$
is not strong enough to make this determination (Zilberstein et al., 2023a).

Similar to the syntactic sugar for probabilistic programs in Section 2.3, we
let $\varphi\oplus_{p}\psi\triangleq\varphi^{(p)}\oplus\psi^{(1-p)}$. If $P$
and $Q$ are the results of running $C_{1}$ and $C_{2}$, then
$P\oplus_{p}Q$—meaning that $P$ occurs with probability $p$ and $Q$ occurs
with probability $1-p$—is the result of running $C_{1}+_{p}C_{2}$.

###  3.2. Outcome Triples

Inspired by Hoare Logic, Outcome Triples
${\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$
specify program behavior in terms of pre- and postconditions (Zilberstein et
al., 2023a). The difference is that Outcome Logic describes weighted
collections of states as opposed to Hoare Logic, which can only describe
individual states. We write
$\vDash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$
to mean that a triple is semantically valid, as defined below.

###### Definition 3.1 (Outcome Triples).

Given
$\langle\mathcal{A},\Sigma,\mathsf{Act},\mathsf{Test},\left\llbracket\cdot\right\rrbracket_{\mathsf{Act}}\rangle$,
the semantics of outcome triples is defined as follows:

$\vDash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}\quad\text{iff}\quad\forall
m\in\mathcal{W}_{\mathcal{A}}(\Sigma).~{}m\vDash\varphi\implies\left\llbracket
C\right\rrbracket^{\dagger}\\!(m)\vDash\psi$

Informally,
${\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$
is valid if the result of running the program $C$ on a weighted collection of
states satisfying $\varphi$ satisfies $\psi$. The power to describe the
collection of states in the postcondition means that Outcome Logic can express
many types of properties including reachability ($P\oplus Q$), probabilities
($P\oplus_{p}Q$), and nontermination (the lack of outcomes,
$\top^{(\dsser{0})}$). Next, we will see how Outcome Logic can be used to
encode familiar program logics.

Commands

$\hypertarget{rule:Skip}{}\inferrule{\;}{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}\mathsf{skip}~{}{\color[rgb]{.75,0,.25}\langle\varphi\rangle}}{\textsc{Skip}}\qquad\qquad\qquad\hypertarget{rule:Seq}{}\inferrule{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\langle\vartheta\rangle}\\\
{\color[rgb]{.75,0,.25}\langle\vartheta\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}}{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C_{1}\fatsemi
C_{2}~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}}{\textsc{Seq}}\qquad\qquad\qquad\hypertarget{rule:Plus}{}\inferrule{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\langle\psi_{1}\rangle}\\\
{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\psi_{2}\rangle}}{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C_{1}+C_{2}~{}{\color[rgb]{.75,0,.25}\langle\psi_{1}\oplus\psi_{2}\rangle}}{\textsc{Plus}}$
$\inferrule{\varphi\vDash
e=u}{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}\mathsf{assume}~{}e~{}{\color[rgb]{.75,0,.25}\langle\varphi^{(u)}\rangle}}{\hypertarget{rule:Assume}{\textsc{Assume}}}\qquad\qquad\inferrule{({\psi}_{n})_{n\in\mathbb{N}}\rightsquigarrow{\psi}_{\infty}\quad\forall
n\in\mathbb{N}.\quad{\color[rgb]{.75,0,.25}\langle\varphi_{n}\rangle}~{}\mathsf{assume}~{}e\fatsemi
C~{}{\color[rgb]{.75,0,.25}\langle\varphi_{n+1}\rangle}\quad{\color[rgb]{.75,0,.25}\langle\varphi_{n}\rangle}~{}\mathsf{assume}~{}e^{\prime}~{}{\color[rgb]{.75,0,.25}\langle\psi_{n}\rangle}}{{\color[rgb]{.75,0,.25}\langle\varphi_{0}\rangle}~{}C^{\langle
e,e^{\prime}\rangle}~{}{\color[rgb]{.75,0,.25}\langle\psi_{\infty}\rangle}}{\hypertarget{rule:Iter}{\textsc{Iter}}}$

Structural Rules

$\begin{array}[]{ccc}\inferrule{\;}{{\color[rgb]{.75,0,.25}\langle\bot\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\varphi\rangle}}{\hypertarget{rule:False}{\textsc{False}}}&\inferrule{\;}{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\top\rangle}}{\hypertarget{rule:True}{\textsc{True}}}&\inferrule{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}}{{\color[rgb]{.75,0,.25}\langle\varphi^{(u)}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi^{(u)}\rangle}}{\hypertarget{rule:Scale}{\textsc{Scale}}}\\\
\\\
\inferrule{{\color[rgb]{.75,0,.25}\langle\varphi_{1}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi_{1}\rangle}\\\
{\color[rgb]{.75,0,.25}\langle\varphi_{2}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi_{2}\rangle}}{{\color[rgb]{.75,0,.25}\langle\varphi_{1}\vee\varphi_{2}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi_{1}\vee\psi_{2}\rangle}}{\hypertarget{rule:Disj}{\textsc{Disj}}}&\inferrule{{\color[rgb]{.75,0,.25}\langle\varphi_{1}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi_{1}\rangle}\\\
{\color[rgb]{.75,0,.25}\langle\varphi_{2}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi_{2}\rangle}}{{\color[rgb]{.75,0,.25}\langle\varphi_{1}\land\varphi_{2}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi_{1}\land\psi_{2}\rangle}}{\hypertarget{rule:Conj}{\textsc{Conj}}}&\inferrule{{\color[rgb]{.75,0,.25}\langle\varphi_{1}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi_{1}\rangle}\\\
{\color[rgb]{.75,0,.25}\langle\varphi_{2}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi_{2}\rangle}}{{\color[rgb]{.75,0,.25}\langle\varphi_{1}\oplus\varphi_{2}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi_{1}\oplus\psi_{2}\rangle}}{\hypertarget{rule:Choice}{\textsc{Choice}}}\end{array}$
$\hypertarget{rule:Cons}{\inferrule{\forall t\in
T.\quad{\color[rgb]{.75,0,.25}\langle\phi(t)\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\phi^{\prime}(t)\rangle}}{{\color[rgb]{.75,0,.25}\langle\exists
x:T.~{}\phi(x)\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\exists
x:T.~{}\phi^{\prime}(x)\rangle}}{\hypertarget{rule:Exists}{\textsc{Exists}}}\qquad\qquad\qquad\inferrule{\varphi^{\prime}\Rightarrow\varphi\\\
{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}\\\
\psi\Rightarrow\psi^{\prime}}{{\color[rgb]{.75,0,.25}\langle\varphi^{\prime}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi^{\prime}\rangle}}{\hypertarget{rule:Consequence}{\textsc{Consequence}}}}$

Figure 3. Rules of inference for Outcome Logic

###  3.3. Dynamic Logic and Hoare Logic

Outcome Logic, in its full generality, allows one to quantify the precise
weights of each outcome. Nevertheless, many common program logics do not
provide this much power, which can be advantageous as they offer simplified
reasoning principles—Hoare Logic’s loop Invariant rule (Section 5.3) is
considerably simpler than the While rule needed for general Outcome Logic
(Section 5.2).

In this section, we devise an assertion syntax in order to show the
connections between Outcome Logic and Hoare Logic. We take inspiration from
modal logic and Dynamic Logic (Pratt, 1976), using the modalities $\Box$ and
$\Diamond$ to express that assertions always or sometimes occur, respectively.
We encode these modalities using the operations from Section 3.1, where $U$ is
the set of semiring weights.

$\begin{array}[]{rclcl}\square P&\triangleq&\exists
u:U.P^{(u)}&=&\\{m\mid\mathsf{supp}(m)\subseteq P\\}\\\ \Diamond
P&\triangleq&\exists
u:(U\setminus\\{\dsser{0}\\}).P^{(u)}\oplus\top&=&\\{m\mid\mathsf{supp}(m)\cap
P\neq\emptyset\\}\end{array}$

We define $\Box P$ to mean that $P$ occurs with some weight, so $m\vDash\Box
P$ exactly when $\mathsf{supp}(m)\subseteq P$. Dually, $\Diamond P$ requires
that $P$ has nonzero weight and the $-\oplus\top$ allows there to be other
elements in the support too. So, $m\vDash\Diamond P$ when $\sigma\vDash P$ for
some $\sigma\in\mathsf{supp}(m)$. It is relatively easy to see that these two
modalities are De Morgan duals, that is $\Box
P\Leftrightarrow\lnot\Diamond\lnot P$ and $\Diamond
P\Leftrightarrow\lnot\Box\lnot P$.

For Boolean-valued semirings (Examples 2.5 and 2.4), we get that $\Box
P=P^{(0)}\vee P^{(1)}$. Only $\dsser{0}$ satisfies $P^{(0)}$, indicating that
the program diverged (let us call this assertion $\mathsf{div}$), and
$P^{(1)}$ is equivalent to $P$. So, $\Box P=P\vee\mathsf{div}$, meaning that
either $P$ covers all the reachable outcomes, or the program diverged ($\Box$
will be useful for expressing partial correctness). Similarly, $\Diamond
P=P\oplus\top$, meaning that $P$ is one of the (possibly many) reachable
outcomes.

Now, we are going to use these modalities to show that Outcome Logic subsumes
other program logics. We start with nondeterministic, partial correctness
Hoare Logic, where the meaning of the triple
${\color[rgb]{.75,0,.25}\\{P\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{Q\\}}$ is
that any state resulting from running the program $C$ on a state satisfying
$P$ must satisfy $Q$. There are many equivalent ways to formally define the
semantics of Hoare Logic; we will use a characterization based on Dynamic
Logic (Pratt, 1976), which is inspired by modal logic in that it defines
modalities similar to $\Box$ and $\Diamond$.

$[C]Q=\\{\sigma\mid\left\llbracket C\right\rrbracket(\sigma)\subseteq
Q\\}\qquad\langle C\rangle Q=\\{\sigma\mid\left\llbracket
C\right\rrbracket(\sigma)\cap Q\neq\emptyset\\}$

That is, $[C]Q$ is an assertion stating that $Q$ must hold after running the
program $C$ (if it terminates). In the predicate transformer literature,
$[C]Q$ is called the weakest liberal precondition (Dijkstra, 1976, 1975). The
dual modality $\langle C\rangle Q$ states that $Q$ might hold after running
$C$ (sometimes referred to as the weakest possible precondition (Hoare, 1978;
Möller et al., 2021)).

A Hoare Triple
${\color[rgb]{.75,0,.25}\\{P\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{Q\\}}$ is
valid iff $P\subseteq[C]Q$, so to show that Outcome Logic subsumes Hoare
Logic, it suffices to prove that we can express $P\subseteq[C]Q$. We do so
using the $\Box$ modality defined previously. More precisely, we capture Hoare
Triples as follows.

###### Theorem 3.2 (Subsumption of Hoare Logic).

$\vDash{\color[rgb]{.75,0,.25}\langle
P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Box
Q\rangle}\qquad\text{iff}\qquad
P\subseteq[C]Q\qquad\text{iff}\qquad\vDash{\color[rgb]{.75,0,.25}\\{P\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{Q\\}}$

While it has already been shown that Outcome Logic subsumes Hoare Logic
(Zilberstein et al., 2023a), our characterization is not tied to
nondeterminism; the triple ${\color[rgb]{.75,0,.25}\langle
P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Box Q\rangle}$ does not
necessarily have to be interpreted in a nondeterministic way, but can rather
be taken to mean that running $C$ in a state satisfying $P$ results in $Q$
covering all the terminating traces with some weight. When we later develop
rules for reasoning about loops using invariants (Section 5), those techniques
will be applicable to _any_ instance of Outcome Logic.

Given that the formula $P\subseteq[C]Q$ gives rise to a meaningful program
logic, it is natural to ask whether the same is true for $P\subseteq\langle
C\rangle Q$. In fact, this formula is colloquially known as Lisbon Logic (it
was proposed during a meeting in Lisbon as a possible foundation for
incorrectness reasoning (O’Hearn, 2019; Möller et al., 2021; Zilberstein et
al., 2023a)). The semantics of Lisbon triples, denoted
${\color[rgb]{.75,0,.25}\\{\\!|P|\\!\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{\\!|Q|\\!\\}}$,
is that for any start state satisfying $P$, there exists a state resulting
from running $C$ that satisfies $Q$. Given that $Q$ only covers a subset of
the outcomes, it is not typically suitable for correctness, however it is
useful for incorrectness as some bugs only occur some of the time.

###### Theorem 3.3 (Subsumption of Lisbon Logic).

$\vDash{\color[rgb]{.75,0,.25}\langle
P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Diamond
Q\rangle}\qquad\text{iff}\qquad P\subseteq\langle C\rangle
Q\qquad\text{iff}\qquad\vDash{\color[rgb]{.75,0,.25}\\{\\!|P|\\!\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{\\!|Q|\\!\\}}$

In the following section, we will see a complete proof system for Outcome
Logic and, given that we have just shown that Outcome Logic subsumes Hoare and
Lisbon Logic, it will allow us to derive any specification in those two logics
as well. However, given the generality of Outcome Logic, some of the proof
rules are not ergonomic for use in less expressive variants. Later, in Section
5, we show how we can derive simpler rules, for example, to analyze loops
using invariants (Hoare Logic) or variants (Lisbon Logic).

##  4\. Proof Theory

We now describe the Outcome Logic rules of inference, which are shown in
Figure 3. The rules are split into three categories.

Standard Commands. The rules for standard (non-looping) commands mostly
resemble those of Hoare Logic. The Skip rule stipulates that the precondition
is preserved after running a no-op. Seq derives a specification for a
sequential composition from two sub-derivations for each command. Similarly,
Plus joins the derivations of two program branches using an outcome
conjunction.

Assume has a side condition that $\varphi\vDash e=u$, where $u\in U$ is a
semiring element. Informally, this means that the precondition entails that
the expression $e$ is some concrete weight $u$. More formally, it is defined
as follows:

$\varphi\vDash e=u\qquad\text{iff}\qquad\forall
m\in\varphi.\quad\forall\sigma\in\mathsf{supp}(m).\quad\left\llbracket
e\right\rrbracket(\sigma)=u$

If $e$ is a weight literal, then $\varphi\vDash u=u$ vacuously holds, so the
rule can be simplified to
$\vdash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}\mathsf{assume}~{}u~{}{\color[rgb]{.75,0,.25}\langle\varphi^{(u)}\rangle}$,
but if it is a test $b$, then $\varphi$ must contain enough information to
conclude that $b$ is true or false. Additional rules to decide $\varphi\vDash
e=u$ are given in Appendix C.

Iteration. The Iter rule uses two families of predicates: $\varphi_{n}$
represents the result of $n$ iterations of $\mathsf{assume}~{}e\fatsemi C$ and
$\psi_{n}$ is the result of iterating $n$ times and then weighting the result
by $e^{\prime}$, so $\bigoplus_{n\in\mathbb{N}}\psi_{n}$ represents all the
terminating traces. To avoid the infinitary outcome conjunction, we instead
use the assertion $\psi_{\infty}$, which must have the following property.

###### Definition 4.1 (Converging Assertions).

A family $(\psi_{n})_{n\in\mathbb{N}}$ _converges_ (written
$({\psi}_{n})_{n\in\mathbb{N}}\rightsquigarrow{\psi}_{\infty}$) iff for any
collection $(m_{n})_{n\in\mathbb{N}}$, if $m_{n}\vDash\psi_{n}$ for each
$n\in\mathbb{N}$, then $\sum_{n\in\mathbb{N}}m_{n}\vDash\psi_{\infty}$.

Structural Rules. We also give additional rules that are not dependent on the
program command. This includes rules for trivial pre- and postconditions (True
and False), scaling by a weight (Scale), combining subderivations using
logical connectives (Disj, Conj, and Choice), introducing existential
quantification (Exists), and weakening (Consequence). Note that the
implications in the rule of Consequence are semantic ones:
$\varphi^{\prime}\Rightarrow\varphi$ iff $\varphi^{\prime}\subseteq\varphi$.
We do not explore the proof theory for outcome assertions, although it has
been done for similar logics (O’Hearn and Pym, 1999; Docherty, 2019).

###  4.1. Soundness and Relative Completeness

Soundness of the Outcome Logic proof system means that any derivable triple
(using the inference rules in Figure 3 and axioms about atomic actions) is
semantically valid. We write
$\Gamma\vdash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$
to mean that
${\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$
is derivable given a collection of axioms
$\Gamma={\color[rgb]{.75,0,.25}\langle\varphi_{1}\rangle}~{}a_{1}~{}{\color[rgb]{.75,0,.25}\langle\psi_{1}\rangle},\ldots,{\color[rgb]{.75,0,.25}\langle\varphi_{n}\rangle}~{}a_{n}~{}{\color[rgb]{.75,0,.25}\langle\psi_{n}\rangle}$.
Let $\Omega$ consist of all triples
${\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}a~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$
such that $a\in\mathsf{Act}$, and
$\vDash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}a~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$
(all the true statements about atomic actions). We also presume that the
program $C$ is well-formed as described in Section 2.3. The soundness theorem
is stated formally below.

###### Theorem 4.2 (Soundness).

$\Omega\vdash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}\implies\vDash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$

The full proof is shown in Appendix C and proceeds by induction on the
structure of the derivation
$\Omega\vdash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$,
with cases in which each rule is the last inference. Most of the cases are
straightforward, but the following lemma is needed to justify the soundness of
the Iter case, where $C^{0}=\mathsf{skip}$ and $C^{n+1}=C^{n}\fatsemi C$.

###### Lemma 4.3.

The following equation holds:

$\left\llbracket{C}^{\langle
e,e^{\prime}\rangle}\right\rrbracket(\sigma)=\sum_{n\in\mathbb{N}}\left\llbracket(\mathsf{assume}~{}e\fatsemi
C)^{n}\fatsemi\mathsf{assume}~{}e^{\prime}\right\rrbracket(\sigma)$

Completeness—the converse of soundness—tells us that our inference rules are
sufficient to deduce any true statement about a program. As is typical,
Outcome Logic is _relatively_ complete, meaning that proving any valid triple
can be reduced to implications $\varphi\Rightarrow\psi$ in the assertion
language. For OL instances involving state (and Hoare Logic), those
implications are undecidable since they must, at the very least, encode Peano
arithmetic (Cook, 1978; Apt, 1981; Lipton, 1977).

The first step is to show that given any program $C$ and precondition
$\varphi$, we can derive the triple
${\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$,
where $\psi$ is the _strongest postcondition_ (Dijkstra and Schölten, 1990),
_i.e.,_ the strongest assertion making that triple true. As defined below,
$\psi$ is exactly the set resulting from evaluating $C$ on each $m\in\varphi$.
The proceeding lemma shows that the triple with the strongest postcondition is
derivable.

###### Definition 4.4 (Strongest Postcondition).

$\mathsf{post}(C,\varphi)\triangleq\\{\left\llbracket
C\right\rrbracket^{\dagger}\\!(m)\mid m\in\varphi\\}$

###### Lemma 4.5.

$\Omega\vdash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\mathsf{post}(C,\varphi)\rangle}$

The proof is by induction on the structure of the program, and is shown in its
entirety in Appendix C. The cases for $\mathsf{skip}$ and $C_{1}\fatsemi
C_{2}$ are straightforward, but the other cases are more challenging and
involve existential quantification. To give an intuition as to why
existentials are needed, let us examine an example involving branching. We use
a concrete instance of Outcome Logic with variable assignment (formalized in
Section 6).

Consider the program $\mathsf{skip}+(x\coloneqq x+1)$ and the precondition
$x\geq 0$. It is tempting to say that $\mathsf{post}$ is obtained
compositionally by joining the $\mathsf{post}$ of the two branches using
$\oplus$:

$\displaystyle\mathsf{post}(\mathsf{skip}+(x\coloneqq x+1),~{}x\geq 0)$
$\displaystyle\quad=\mathsf{post}(\mathsf{skip},x\geq
0)\oplus\mathsf{post}(x:=x+1,~{}x\geq 0)$ $\displaystyle\quad=(x\geq
0)\oplus(x\geq 1)$

However, that is incorrect. While it is a valid postcondition, it is not the
strongest one because it does not account for the relationship between the
values of $x$ in the two branches; if $x=n$ in the first branch, then it must
be $n+1$ in the second branch. A second attempt could use existential
quantification to dictate that relationship.

$\exists n:\mathbb{N}.~{}(x=n)\oplus(x=n+1)$

Unfortunately, that is also incorrect; it does not properly account for the
fact that that precondition $x\geq 0$ may be satisfied by a _set_ of states in
which $x$ has many different values—the existential quantifier requires that
$x$ takes on a single value in all the initial outcomes. The solution is to
quantify over the collections $m\in\varphi$ satisfying the precondition, and
then to take the $\mathsf{post}$ of $\mathbf{1}_{m}=\\{m\\}$.

$\mathsf{post}(C_{1}+C_{2},\varphi)=\exists
m:\varphi.~{}\mathsf{post}(C_{1},\mathbf{1}_{m})\oplus\mathsf{post}(C_{2},\mathbf{1}_{m})$

While it may seem unwieldy that the strongest post is hard to characterize
even in this seemingly innocuous example, the same problem arises in logics
for probabilistic (Barthe et al., 2018; den Hartog, 2002) and hyper-property
(Dardinier and Müller, 2023) reasoning, both of which are instances of OL.
Although the _strongest_ postcondition is quite complicated, something weaker
suffices in most cases. We will later see how rules for those simpler cases
are derived (Section 5) and used (Sections 7 and 8).

The main result is now a straightforward corollary of Lemma 4.5 using the rule
of Consequence, since any valid postcondition is implied by the strongest one.

###### Theorem 4.6 (Relative Completeness).

$\vDash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}\implies\Omega\vdash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$

###### Proof.

We first establish that $\mathsf{post}(C,\varphi)\Rightarrow\psi$. Suppose
that $m\in\mathsf{post}(C,\varphi)$. That means that there must be some
$m^{\prime}\in\varphi$ such that $m=\left\llbracket
C\right\rrbracket^{\dagger}\\!(m^{\prime})$. Using
$\vDash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$,
we get that $m\vDash\psi$. Now, we complete the derivation as follows:

$\inferrule*[right=\hyperlink{rule:Consequence}{\textsc{Consequence}}]{\inferrule*[right=\lx@cref{creftypecap~refnum}{lem:completeness}]{\Omega}{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\mathsf{post}(C,\varphi)\rangle}}\quad\mathsf{post}(C,\varphi)\Rightarrow\psi}{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}}$

∎

##  5\. Derived Rules

We now present derived rules for simplified reasoning involving if statements,
while loops, and the encodings of Hoare and Lisbon Logic from Section 3.3.
Recall that Hoare triples
${\color[rgb]{.75,0,.25}\\{P\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{Q\\}}$ are
semantically equivalent to ${\color[rgb]{.75,0,.25}\langle
P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Box Q\rangle}$ in Outcome Logic
(Theorem 3.2) and Lisbon triples
${\color[rgb]{.75,0,.25}\\{\\!|P|\\!\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{\\!|Q|\\!\\}}$
are equivalent to ${\color[rgb]{.75,0,.25}\langle
P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Diamond Q\rangle}$ (Theorem
3.3). For the full derivations, refer to Appendix D.

###  5.1. Sequencing in Hoare and Lisbon Logic

The Seq rule requires that the postcondition of the first command exactly
matches the precondition of the next. This is at odds with our encodings of
Hoare and Lisbon Logic, which have asymmetry between the modalities used in
the pre- and postconditions. Still, sequencing is possible using derived
rules.

$\inferrule{{\color[rgb]{.75,0,.25}\langle
P\rangle}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\langle\Box Q\rangle}\\\
{\color[rgb]{.75,0,.25}\langle
Q\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\Box
R\rangle}}{{\color[rgb]{.75,0,.25}\langle P\rangle}~{}C_{1}\fatsemi
C_{2}~{}{\color[rgb]{.75,0,.25}\langle\Box R\rangle}}{\hypertarget{rule:Seq
(Hoare)}{\textsc{Seq (Hoare)}}}$ $\inferrule{{\color[rgb]{.75,0,.25}\langle
P\rangle}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\langle\Diamond Q\rangle}\\\
{\color[rgb]{.75,0,.25}\langle
Q\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\Diamond
R\rangle}}{{\color[rgb]{.75,0,.25}\langle P\rangle}~{}C_{1}\fatsemi
C_{2}~{}{\color[rgb]{.75,0,.25}\langle\Diamond
R\rangle}}{\hypertarget{rule:Seq (Lisbon)}{\textsc{Seq (Lisbon)}}}$

Since both $\Box$ and $\Diamond$ are encoded using existential quantifiers,
the derivations (Section D.1) use Scale and Exists to conclude:

$\displaystyle{\color[rgb]{.75,0,.25}\langle
Q\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\Box R\rangle}$
$\displaystyle\quad\vdash\quad{\color[rgb]{.75,0,.25}\langle
Q^{(v)}\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\exists u:U.R^{(u\cdot
v)}\rangle}$
$\displaystyle\quad\vdash\quad{\color[rgb]{.75,0,.25}\langle\exists
v:U.Q^{(v)}\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\exists
v,u:U.R^{(u\cdot v)}\rangle}$
$\displaystyle\quad\vdash\quad{\color[rgb]{.75,0,.25}\langle\Box
Q\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\Box R\rangle}$

The case for $\Diamond$ is similar, also making use of the fact that
$-\oplus\top$ is idempotent ($(R\oplus\top)\oplus\top\Leftrightarrow
R\oplus\top$). Lisbon Logic adds an additional requirement on the semiring;
$\dsser{0}$ must be the _unique_ annihilator of multiplication ($u\cdot
v=\dsser{0}$ iff $u=\dsser{0}$ or $v=\dsser{0}$), which ensures that a finite
sequence of commands does not eventually cause a branch to have zero weight.
Examples 2.5, 2.4, 2.6, 2.7 and 2.8 all obey this property.

###  5.2. If Statements and While Loops

Recall from Section 2.3 that we encode if statements and while loops using the
choice and iteration constructs. We now derive convenient inference rules for
those cases. If statements are defined as $(\mathsf{assume}~{}b\fatsemi
C_{1})+(\mathsf{assume}~{}\lnot b\fatsemi C_{2})$. Reasoning about them
generally requires the precondition to be separated into two parts,
$\varphi_{1}$ and $\varphi_{2}$, representing the collections of states in
which $b$ is true and false, respectively. This may require— _e.g.,_ in the
probabilistic case—that $\varphi_{1}$ and $\varphi_{2}$ quantify the weight
(likelihood) of the guard.

If it is possible to separate the precondition in that way, then $\varphi_{1}$
and $\varphi_{2}$ act as the preconditions for $C_{1}$ and $C_{2}$,
respectively, and the overall postcondition is an outcome conjunction of the
results of both branches.

$\inferrule{\varphi_{1}\vDash b\\\
{\color[rgb]{.75,0,.25}\langle\varphi_{1}\rangle}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\langle\psi_{1}\rangle}\\\
\varphi_{2}\vDash\lnot b\\\
{\color[rgb]{.75,0,.25}\langle\varphi_{2}\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\psi_{2}\rangle}}{{\color[rgb]{.75,0,.25}\langle\varphi_{1}\oplus\varphi_{2}\rangle}~{}\mathsf{if}~{}b~{}\mathsf{then}~{}C_{1}~{}\mathsf{else}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\psi_{2}\oplus\psi_{2}\rangle}}{\hypertarget{rule:If}{\textsc{If}}}$

From If, we derive the familiar rules for Hoare and Lisbon Logic.

$\inferrule{{\color[rgb]{.75,0,.25}\langle P\land
b\rangle}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\langle\Box
Q\rangle}\quad{\color[rgb]{.75,0,.25}\langle P\land\lnot
b\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\Box
Q\rangle}}{{\color[rgb]{.75,0,.25}\langle
P\rangle}~{}\mathsf{if}~{}b~{}\mathsf{then}~{}C_{1}~{}\mathsf{else}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\Box
Q\rangle}}{\hypertarget{rule:If (Hoare)}{\textsc{If (Hoare)}}}$
$\inferrule{{\color[rgb]{.75,0,.25}\langle P\land
b\rangle}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\langle\Diamond
Q\rangle}\quad{\color[rgb]{.75,0,.25}\langle P\land\lnot
b\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\Diamond
Q\rangle}}{{\color[rgb]{.75,0,.25}\langle
P\rangle}~{}\mathsf{if}~{}b~{}\mathsf{then}~{}C_{1}~{}\mathsf{else}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\langle\Diamond
Q\rangle}}{\hypertarget{rule:If (Lisbon)}{\textsc{If (Lisbon)}}}$

The derivations rely on the fact that if $P$ holds, then there exist $u$ and
$v$ such that $u+v=\dsser{1}$ and $(P\land b)^{(u)}\oplus(P\land\lnot
b)^{(v)}$ holds. We complete the proof using Scale and Split, and
existentially quantify the new weights using $\Box$ and $\Diamond$.

The rule for while loops is slightly simplified compared to Iter, as it only
generates a proof obligation for a single triple instead of two. There are
still two families of assertions, but $\varphi_{n}$ now represents the portion
of the program configuration where the guard $b$ is true, and $\psi_{n}$
represents the portion where it is false. So, on each iteration, $\varphi_{n}$
continues to evaluate and $\psi_{n}$ exits; the final postcondition
$\psi_{\infty}$ is an aggregation of all the terminating traces.

$\inferrule{({\psi}_{n})_{n\in\mathbb{N}}\rightsquigarrow{\psi}_{\infty}\quad{\color[rgb]{.75,0,.25}\langle\varphi_{n}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\varphi_{n+1}\oplus\psi_{n+1}\rangle}\quad\varphi_{n}\vDash
b\quad\psi_{n}\vDash\lnot
b}{{\color[rgb]{.75,0,.25}\langle\varphi_{0}\oplus\psi_{0}\rangle}~{}\mathsf{while}~{}b~{}\mathsf{do}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi_{\infty}\rangle}}{\hypertarget{rule:While}{\textsc{While}}}$

This While rule is similar to those found in probabilistic Hoare Logics (den
Hartog, 1999; Barthe et al., 2018).

###  5.3. Loop Invariants

Loop invariants are a popular analysis technique in partial correctness
logics. The idea is to find an invariant $P$ that is preserved by the loop
body and therefore must remain true when— _and if_ —the loop terminates.
Because loop invariants are unable to guarantee termination, the Outcome Logic
rule must indicate that the program may diverge. We achieve this using the
$\Box$ modality from Section 3.3. The rule for Outcome Logic loop invariants
is as follows:

$\inferrule{{\color[rgb]{.75,0,.25}\langle P\land
b\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Box
P\rangle}}{{\color[rgb]{.75,0,.25}\langle
P\rangle}~{}\mathsf{while}~{}b~{}\mathsf{do}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Box(P\land\lnot
b)\rangle}}{\hypertarget{rule:Invariant}{\textsc{Invariant}}}$

This rule states that if the program starts in a state described by $P$, which
is also preserved by each execution of the loop, then $P\land\lnot b$ is true
of every reachable end state. If the program diverges and there are no
reachable end states, then $\Box(P\land\lnot b)$ is vacuously satisfied, just
like in Hoare Logic.

Invariant is derived using the While rule with $\varphi_{n}=\Box(P\land b)$
and $\psi_{n}=\Box(P\land\lnot b)$. To show
$({\psi}_{n})_{n\in\mathbb{N}}\rightsquigarrow{\psi}_{\infty}$, first note
that $m_{n}\vDash\Box(P\land\lnot b)$ simply means that
$\mathsf{supp}(m_{n})\subseteq(P\land\lnot b)$. Since this is true for all
$n\in\mathbb{N}$, then all the reachable states satisfy $P\land\lnot b$.

In Section 3.3 we used ${\color[rgb]{.75,0,.25}\langle
P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Box Q\rangle}$ to encode
nondeterministic Hoare Logic, but the Invariant rule applies to all instances
of Outcome Logic. For example, this rule can be used for probabilistic
programs to state that $P\land\lnot b$ covers all the terminating outcomes,
and occurs with some probability.

It is well known that Skip, Seq (Hoare), If (Hoare), Invariant, and
Consequence constitute a complete proof system for Hoare Logic (Cook, 1978;
Kozen and Tiuryn, 2001). It follows that these rules are also complete for
deriving any Outcome Logic triples of the form ${\color[rgb]{.75,0,.25}\langle
P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Box Q\rangle}$, avoiding the
more complex machinery of Lemma 4.5444 _N.B._ , this only includes the
deterministic program constructs—if statements and while loops instead of
$C_{1}+C_{2}$ and ${C}^{\langle e,e^{\prime}\rangle}$. The inclusion of a few
more derived rules completes the proof system for nondeterministic programs.

###  5.4. Loop Variants

Loop variants are an alternative way to reason about loops when termination
guarantees are needed. They were first studied in the context of total Hoare
Logic (Manna and Pnueli, 1974), but are also used in other logics that require
termination guarantees such as Reverse Hoare Logic (de Vries and Koutavas,
2011), Incorrectness Logic (O’Hearn, 2019), and Lisbon Logic (Möller et al.,
2021; Raad et al., 2023; Ascari et al., 2023).555 Outcome Logic guarantees the
_existence_ of terminating traces, but it is not a total correctness logic in
that it cannot ensure that _all_ traces terminate. This stems from the program
semantics, which collects the finite traces, but does not preclude additional
nonterminating ones. For example,
$\left\llbracket\mathsf{skip}\right\rrbracket(\sigma)=\left\llbracket\mathsf{skip}+\mathsf{while}~{}\mathsf{true}~{}\mathsf{do}~{}\mathsf{skip}\right\rrbracket(\sigma)$.
The exception is the probabilistic interpretation, where _almost sure
termination_ can be established by proving that the weight of the
postcondition is 1.

Rather than using an invariant that is preserved by the loop body, we now use
a family of changing _variants_ $(\varphi_{n})_{n\in\mathbb{N}}$ such that
$\varphi_{n}$ implies that the loop guard $b$ is true for all $n>0$, and
$\varphi_{0}$ implies that it is false, guaranteeing that the loop exits. The
inference rule is shown below, and states that starting at some $\varphi_{n}$,
the execution will eventually count down to $\varphi_{0}$, at which point it
terminates.

$\inferrule{\forall n\in\mathbb{N}.\\\ \varphi_{0}\vDash\lnot b\\\
\varphi_{n+1}\vDash b\\\
{\color[rgb]{.75,0,.25}\langle\varphi_{n+1}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\varphi_{n}\rangle}}{{\color[rgb]{.75,0,.25}\langle\exists
n:\mathbb{N}.\varphi_{n}\rangle}~{}\mathsf{while}~{}b~{}\mathsf{do}~{}C~{}{\color[rgb]{.75,0,.25}\langle\varphi_{0}\rangle}}{\hypertarget{rule:Variant}{\textsc{Variant}}}$

Since the premise guarantees termination after precisely $n$ steps, it is easy
to establish convergence—the postcondition only consists of a single trace.

Although loop variants are valid in any Outcome Logic instance, they require
loops to be _deterministic_ —the loop executes for the same number of
iterations regardless of any computational effects that occur in the body.
Examples of such scenarios include for loops, where the number of iterations
is fixed upfront.

We also present a more flexible loop variant rule geared towards Lisbon
triples. In this case, we use the $\Diamond$ modality to only require that
_some_ trace is moving towards termination.

$\inferrule{\forall n\in\mathbb{N}.\quad P_{0}\vDash\lnot b\quad P_{n+1}\vDash
b\quad{\color[rgb]{.75,0,.25}\langle
P_{n+1}\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Diamond
P_{n}\rangle}}{{\color[rgb]{.75,0,.25}\langle\exists
n:\mathbb{N}.P_{n}\rangle}~{}\mathsf{while}~{}b~{}\mathsf{do}~{}C~{}{\color[rgb]{.75,0,.25}\langle\Diamond
P_{0}\rangle}}{\hypertarget{rule:Lisbon Variant}{\textsc{Lisbon Variant}}}$

In other words, Lisbon Variant witnesses a single terminating trace. As such,
it does not require the lockstep termination of all outcomes like Variant
does.

##  6\. Adding Variables and State

We now develop a concrete Outcome Logic instance with variable assignment as
atomic actions. Let $\mathsf{Var}$ be a countable set of variable names and
$\mathsf{Val}=\mathbb{Z}$ be integer program values. Program stores
$s\in\mathcal{S}\triangleq\mathsf{Var}\to\mathsf{Val}$ are maps from variables
to values and we write $s[x\mapsto v]$ to denote the store obtained by
extending $s\in\mathcal{S}$ such that $x$ has value $v$. Actions
$a\in\mathsf{Act}$ are variable assignments $x\coloneqq E$, where
$x\in\mathsf{Var}$ and $E$ can be a variable $x\in\mathsf{Var}$, constant
$v\in\mathsf{Val}$, test $b$, or an arithmetic operation ($+$, $-$, $\times$).

$\displaystyle a\in\mathsf{Act}$ $\displaystyle\Coloneqq x\coloneqq E$
$\displaystyle E$ $\displaystyle\Coloneqq x\in\mathsf{Var}\mid
v\in\mathsf{Val}\mid b\mid E_{1}+E_{2}\mid E_{1}-E_{2}\mid E_{1}\times E_{2}$

In addition, we let the set of primitive tests
$\mathsf{Test}=\dsser{2}^{\mathcal{S}}$ be all subsets of the program states
$\mathcal{S}$. We will often write these tests symbolically, for example
$x\geq 5$ represents the set $\\{s\in\mathcal{S}\mid s(x)\geq 5\\}$. The
interpretation of atomic actions is shown below, where the interpretation of
expressions $\left\llbracket
E\right\rrbracket_{\mathsf{Exp}}\colon\mathcal{S}\to\mathsf{Val}$ is in
Appendix E.

$\left\llbracket x\coloneqq
E\right\rrbracket_{\mathsf{Act}}(s)\triangleq\eta(s[x\mapsto\left\llbracket
E\right\rrbracket_{\mathsf{Exp}}(s)])$

We define substitutions in the standard way (Dardinier and Müller, 2023;
Barthe et al., 2018; Ascari et al., 2023; Kaminski, 2019), as follows:

$\varphi[E/x]\triangleq\\{m\in\mathcal{W}(\mathcal{S})\mid(\lambda
s.\eta(s[x\mapsto\left\llbracket
E\right\rrbracket_{\mathsf{Exp}}(s))])^{\dagger}(m)\in\varphi\\}$

That is, $m\in\varphi[E/x]$ exactly when assigning $x$ to $E$ in $m$ satisfies
$\varphi$. This behaves as expected in conjunction with symbolic tests, for
example $(x\geq 5)[y+1/x]=(y+1\geq 5)=(y\geq 4)$. It also distributes over
most of the operations in Figure 2, _e.g.,_
$(\varphi\oplus\psi)[E/x]=\varphi[E/x]\oplus\psi[E/x]$. Using substitution, we
add an inference rule for assignment, mirroring the typical weakest-
precondition style rule of Hoare Logic (Hoare, 1969).

$\inferrule{\;}{{\color[rgb]{.75,0,.25}\langle\varphi[E/x]\rangle}~{}x\coloneqq
E~{}{\color[rgb]{.75,0,.25}\langle\varphi\rangle}}{\hypertarget{rule:Assign}{\textsc{Assign}}}$

When used in combination with the rule of Consequence, Assign can be used to
derive any semantically valid triple about variable assignment. Though it is
not needed for completeness, we also include the rule of Constancy, which
allows us to add information about unmodified variables to a completed
derivation. Here, $\mathsf{free}(P)$ is the set of _free variables_ that are
used by the assertion $P$ (_e.g.,_ $\mathsf{free}(x\geq 5)=\\{x\\}$) and
$\mathsf{mod}(C)$ are the variables modified by $C$, both defined in Appendix
E. The $\Box$ modality guarantees that the rule applies regardless of whether
or not $C$ terminates.

$\inferrule{{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}\\\
\mathsf{free}(P)\cap\mathsf{mod}(C)=\emptyset}{{\color[rgb]{.75,0,.25}\langle\varphi\land\Box
P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\land\Box
P\rangle}}{\hypertarget{rule:Constancy}{\textsc{Constancy}}}$

In this particular Outcome Logic instance, all triples can be derived without
the axioms $\Omega$ from Theorem 4.6.

###### Theorem 6.1 (Soundness and Completeness).

$\vDash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}\qquad\iff\qquad\vdash{\color[rgb]{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\langle\psi\rangle}$

##  7\. Case Study: Reusing proof Fragments

The following case study serves as a proof of concept for how Outcome Logic’s
unified reasoning principles can benefit large-scale program analysis. The
efficiency of such systems relies on pre-computing procedure specifications,
which can simply be inserted whenever those procedures are invoked rather than
being recomputed at every call-site. Present analysis systems operate over
homogenous effects. Moreover—when dealing with nondeterministic programs—they
must also fix either a demonic interpretation (for correctness) or an angelic
interpretation (for bug-finding).

But many procedures do not have effects—they do not branch into multiple
outcomes and use only limited forms of looping where termination is easily
established (_e.g.,_ iterating over a data structure)—suggesting that
specifications for such procedures can be reused across multiple types of
programs (_e.g.,_ nondeterministic or probabilistic) and specifications
(_e.g.,_ partial or total correctness). Indeed, this is the case for the
program in Section 7.1. We then show how a single proof about that program can
be reused in both a partial correctness specification (Section 7.2) and a
probabilistic program (Section 7.3). The full derivations are given in
Appendix F.

###  7.1. Integer Division

In order to avoid undefined behavior related to division by zero, our
expression syntax from Section 6 does not include division. However, we can
write a simple procedure to divide two natural numbers $a$ and $b$ using
repeated subtraction.

$\mathsf{DIV}\triangleq\left\\{\begin{array}[]{l}q\coloneqq 0\fatsemi
r\coloneqq a\fatsemi\phantom{x}\\\ \mathsf{while}~{}r\geq b~{}\mathsf{do}\\\
\quad r\coloneqq r-b\fatsemi\phantom{x}\\\ \quad q\coloneqq
q+1\end{array}\right.$

At the end of the execution, $q$ holds the quotient and $r$ is the remainder.
Although the $\mathsf{DIV}$ program uses a while loop, it is quite easy to
establish that it terminates. To do so, we use the Variant rule with the
family of variants $\varphi_{n}$ shown below.

$\varphi_{n}\triangleq\left\\{\begin{array}[]{lll}q+n=\lfloor a\div
b\rfloor\land r=(a\bmod b)+n\times b&\text{if}&n\leq\lfloor a\div b\rfloor\\\
\mathsf{false}&\text{if}&n>\lfloor a\div b\rfloor\end{array}\right.$

Executing the loop body in a state satisfying $\varphi_{n}$ results in a state
satisfying $\varphi_{n-1}$. At the end, $\varphi_{0}$ stipulates that
$q=\lfloor a\div b\rfloor$ and $r=a\bmod b$, which immediately implies that
$r<b$, so the loop must exit. This allows us to give the following
specification for the program.

${\color[rgb]{.75,0,.25}\langle a\geq 0\land
b>0\rangle}~{}\mathsf{DIV}~{}{\color[rgb]{.75,0,.25}\langle q=\lfloor a\div
b\rfloor\land r=a\bmod b\rangle}$

Note that the $\mathsf{DIV}$ program is fully deterministic; we did not make
any assumptions about which interpretation of choice is used. This will allow
us to reuse the proof of $\mathsf{DIV}$ in programs with different kinds of
effects in the remainder of the section.

###  7.2. The Collatz Conjecture

Consider the function $f$ defined below.

$f(n)\triangleq\left\\{\begin{array}[]{lll}n\div 2&\text{if}&n\bmod 2=0\\\
3n+1&\text{if}&n\bmod 2=1\end{array}\right.$

The Collatz Conjecture—an elusive open problem in the field of
mathematics—postulates that for any positive $n$, repeated applications of $f$
will eventually yield the value 1. Let the _stopping time_ $S_{n}$ be the
minimum number of applications of $f$ to $n$ that it takes to reach 1. For
example, $S_{1}=0$, $S_{2}=1$, and $S_{3}=7$. When run in an initial state
where $a=n$, the following program computes $S_{n}$, storing the result in
$i$. Note that this program makes use of $\mathsf{DIV}$, defined previously.

$\mathsf{COLLATZ}\triangleq\left\\{\begin{array}[]{l}i\coloneqq
0\fatsemi\phantom{x}\\\ \mathsf{while}~{}a\neq 1~{}\mathsf{do}\\\ \quad
b\coloneqq 2\fatsemi\mathsf{DIV}\fatsemi\phantom{x}\\\
\quad\mathsf{if}~{}r=0~{}\mathsf{then}~{}a\coloneqq
q~{}\mathsf{else}~{}a\coloneqq 3\times a+1\fatsemi\phantom{x}\\\ \quad
i\coloneqq i+1\end{array}\right.$

Since some numbers may not have a finite stopping time—in which case the
program will not terminate—this is a perfect candidate for a partial
correctness proof. Assuming that $a$ initially holds the value $n$, we can use
a loop invariant stating that $a=f^{i}(n)$ on each iteration. _If_ the program
terminates, then $a=f^{i}(n)=1$, and so $S_{n}=i$. We capture this using the
following triple, where the $\Box$ modality indicates that the program may
diverge.

${\color[rgb]{.75,0,.25}\langle a=n\land
n>0\rangle}~{}\mathsf{COLLATZ}~{}{\color[rgb]{.75,0,.25}\langle\Box(i=S_{n})\rangle}$

###  7.3. Embedding Division in a Probabilistic Program

The following program loops for a random number of iterations, deciding
whether to continue by flipping a fair coin. It is interpreted using the
$\mathsf{Prob}$ semiring from Example 2.7.

$a\coloneqq 0\fatsemi r\coloneqq 0\fatsemi\left(a\coloneqq a+1\fatsemi
b\coloneqq 2\fatsemi\mathsf{DIV}\right)^{\langle\frac{1}{2}\rangle}$

Suppose we want to know the probability that it terminates after an even or
odd number of iterations. The program makes use of $\mathsf{DIV}$ to divide
the current iteration number $a$ by 2, therefore the remainder $r$ will
indicate whether the program looped an even or odd number of times. We can
analyze the program with the Iter rule, using the following two families of
assertions.

$\displaystyle\varphi_{n}$ $\displaystyle\triangleq(a=n\land r=a\bmod
2)^{(\frac{1}{2^{n}})}$ $\displaystyle\psi_{n}$
$\displaystyle\triangleq(a=n\land r=a\bmod 2)^{(\frac{1}{2^{n+1}})}$

According to Iter, the final postcondition can be obtained by taking an
outcome conjunction of all the $\psi_{n}$ for $n\in\mathbb{N}$. However, we do
not care about the precise value of $a$, only whether $r$ is 0 or 1. The
probability that $r=0$ is $\frac{1}{2}+\frac{1}{8}+\frac{1}{32}+\cdots$, a
geometric series whose sum converges to $\frac{2}{3}$. A similar calculation
for the $r=1$ case gives us the following specification, indicating that the
program terminates after an even or odd number of iterations with probability
$\frac{2}{3}$ and $\frac{1}{3}$, respectively.

$\begin{array}[]{l}{\color[rgb]{.75,0,.25}\langle\mathsf{true}\rangle}\\\
\quad{a\coloneqq 0\fatsemi r\coloneqq 0\fatsemi\left(a\coloneqq a+1\fatsemi
b\coloneqq 2\fatsemi\mathsf{DIV}\right)^{\langle\frac{1}{2}\rangle}}\\\
{\color[rgb]{.75,0,.25}\langle(r=0)\oplus_{\frac{2}{3}}(r=1)\rangle}\end{array}$

##  8\. Case Study: Graph Problems and Quantitative Analysis

We now examine case studies using Outcome Logic to derive quantitative
properties in alternative models of computation.

###  8.1. Counting Random Walks

Suppose we wish to count the number of paths between the origin and the point
$(N,M)$ on a two dimensional grid. To achieve this, we first write a program
that performs a random walk on the grid; while the destination is not yet
reached, it nondeterministically chooses to take a step on either the $x$ or
$y$-axis (or steps in a fixed direction if the destination on one axis is
already reached).

$\mathsf{WALK}\triangleq\left\\{\begin{array}[]{l}\mathsf{while}~{}x<N\vee
y<M~{}\mathsf{do}\\\ \quad\mathsf{if}~{}x<N\land y<M~{}\mathsf{then}\\\
\quad\quad(x\coloneqq x+1)+(y\coloneqq y+1)\\\ \quad\mathsf{else\ if}~{}x\geq
N~{}\mathsf{then}\\\ \quad\quad y\coloneqq y+1\\\ \quad\mathsf{else}\\\
\quad\quad x\coloneqq x+1\end{array}\right.$

Using a standard program logic, it is relatively easy to prove that the
program will always terminate in a state where $x=N$ and $y=M$. However, we
are going to interpret this program using the $\mathsf{Nat}$ semiring (Example
2.6) in order to count how many traces (_i.e.,_ random walks) reach that
outcome.

First of all, we know it will take exactly $N+M$ steps to reach the
destination, so we can analyze the program using the Variant rule, where the
loop variant $\varphi_{n}$ records the state of the program $n$ steps away
from reaching $(N,M)$.

If we are $n$ steps away, then there are several outcomes ranging from
$x=N-n\land y=M$ to $x=N\land y=M-n$. More precisely, let $k$ be the distance
to $N$ on the $x$-axis, meaning that the distance to $M$ on the $y$-axis must
be $n-k$, so $x=N-k$ and $y=M-(n-k)$. At all times, it must be true that
$0\leq x\leq N$ and $0\leq y\leq M$, so it must also be true that $0\leq
N-k\leq N$ and $0\leq M-(n-k)\leq M$. solving for $k$, we get that $0\leq
k\leq N$ and $n-M\leq k\leq n$. So, $k$ can range between $\max(0,n-M)$ and
$\min(N,n)$.

In addition, the number of paths to $(x,y)$ is ${x+y\choose x}$, _i.e.,_ the
number of ways to pick $x$ steps on the $x$-axis out of $x+y$ total steps.
Putting all of that together, we define our loop variant as follows:

$\varphi_{n}\triangleq\smashoperator[]{\bigoplus_{k=\max(0,n-M)}^{\min(N,n)}}(x=N-k\land
y=M-(n-k))^{({N+M-n\choose N-k})}$

The loop body moves the program state from $\varphi_{n+1}$ to $\varphi_{n}$.
The outcomes of $\varphi_{n+1}$ get divided among the three if branches. In
the outcome where $x=N$ already, $y$ must step, so this goes to the second
branch. Similarly, if $y=M$ already, then $x$ must step, corresponding to the
third branch. All other outcomes go to the first branch, which further splits
into two outcomes due to the nondeterministic choice.

Since we start $N+M$ steps from the destination, we get the following
precondition:

$\varphi_{N+M}=\bigoplus_{k=N}^{N}(x=N-k\land y=N-k)^{({0\choose
N-N})}=(x=0\land y=0)$

In addition, the postcondition is:

$\varphi_{0}=\bigoplus_{k=0}^{0}(x=N-k\land y=M+k)^{({N+M\choose
N})}=(x=N\land y=M)^{({N+M\choose N})}$

This gives us the final specification below, which tells us that there are
${N+M\choose N}$ paths to reach $(N,M)$ from the origin. The full derivation
is given in Section G.1.

${\color[rgb]{.75,0,.25}\langle x=0\land
y=0\rangle}~{}\mathsf{WALK}~{}{\color[rgb]{.75,0,.25}\langle(x=N\land
y=M)^{({N+M\choose N})}\rangle}$

###  8.2. Shortest Paths

We will now use an alternative interpretation of computation to analyze a
program that nondeterministically finds the shortest path from $s$ to $t$ in a
directed graph. Let $G$ be the $N\times N$ Boolean adjacency matrix of a
directed graph, so that $G[i][j]=\mathsf{true}$ if there is an edge from $i$
to $j$ (or $\mathsf{false}$ if no such edge exists). We also add the following
expression syntax to read edge weights in a program, noting that
$G[E_{1}][E_{2}]\in\mathsf{Test}$ since it is Boolean-valued.

$E::=\cdots\mid G[E_{1}][E_{2}]$ $\left\llbracket
G[E_{1}][E_{2}]\right\rrbracket_{\mathsf{Exp}}(s)\triangleq
G\left[\left\llbracket
E_{1}\right\rrbracket_{\mathsf{Exp}}(s)\right]\left[\left\llbracket
E_{2}\right\rrbracket_{\mathsf{Exp}}(s)\right]$

The following program loops until the current position $pos$ reaches the
destination $t$. At each step, it nondeterministically chooses which edge
($next)$ to traverse using an iterator; for all $next\leq N$, each trace is
selected if there is an edge from $pos$ to $next$, and a weight of 1 is then
added to the path, signifying that we took a step.

$\mathsf{SP}\triangleq\left\\{\begin{array}[]{l}\mathsf{while}~{}pos\neq
t~{}\mathsf{do}\\\ \quad next\coloneqq 1\fatsemi\phantom{x}\\\
\quad{\left(next\coloneqq next+1\right)}^{\langle
next<N,~{}G[pos][next]\rangle}\fatsemi\phantom{x}\\\ \quad pos\coloneqq
next\fatsemi\phantom{x}\\\ \quad\mathsf{assume}~{}1\end{array}\right.$

We will interpret this program using the $\mathsf{Tropical}$ semiring from
Example 2.8, in which addition corresponds to $\min$ and multiplication
corresponds to addition. So, path lengths get accumulated via addition and
nondeterministic choices correspond to taking the path with minimal weight.
That means that at the end of the program execution, we should end up in a
scenario where $pos=t$, with weight equal to the shortest path length from $s$
to $t$.

To prove this, we first formalize the notion of shortest paths below:
$\mathsf{sp}^{t}_{n}(G,s,s^{\prime})$ indicates whether there is a path of
length $n$ from $s$ to $s^{\prime}$ in $G$ in without passing through $t$ and
$\mathsf{sp}(G,s,t)$ is the shortest path length from $s$ to $t$. Let
$I=\\{1,\ldots,N\\}\setminus\\{t\\}$.

$\displaystyle\mathsf{sp}_{0}^{t}(G,s,s^{\prime})$
$\displaystyle\triangleq(s=s^{\prime})$
$\displaystyle\mathsf{sp}_{n+1}^{t}(G,s,s^{\prime})$
$\displaystyle\triangleq\smashoperator[]{\bigvee_{i\in
I}^{}}\mathsf{sp}_{n}^{t}(G,s,i)\land G[i][s^{\prime}]$
$\displaystyle\mathsf{sp}(G,s,t)$
$\displaystyle\triangleq{\min{\\{n\in\mathbb{N}\mid\mathsf{sp}_{n}^{t}(G,s,t)\\}}}$

We analyze the while loop using the While rule, which requires $\varphi_{n}$
and $\psi_{n}$ to record the outcomes where the loop guard is true or false,
respectively, after $n$ iterations. We define these as follows:

$\varphi_{n}=\smashoperator[]{\bigoplus_{i\in
I}^{}}(pos=i)^{(\mathsf{sp}_{n}^{t}(G,s,i)+n)}$
$\psi_{n}=(pos=t)^{(\mathsf{sp}_{n}^{t}(G,s,t)+n)}\qquad\psi_{\infty}=(pos=t)^{(\mathsf{sp}(G,s,t))}$

Recall that in the tropical semiring $\mathsf{false}=\infty$ and
$\mathsf{true}=0$. So, after $n$ iterations, the weight of the outcome $pos=i$
is equal to $n$ if there is an $n$-step path from $s$ to $i$, and $\infty$
otherwise. The final postcondition $\psi_{\infty}$ is the shortest path length
to $t$, which is also the minimum of $\mathsf{sp}_{n}^{t}(G,s,t)+n$ for all
$n$. Using the Iter rule we get the following derivation for the inner loop:

$\begin{array}[]{l}{\color[rgb]{.75,0,.25}\left\langle\bigoplus_{i\in
I}(pos=i\land next=1)^{(\mathsf{sp}_{n}^{t}(G,s,i)+n)}\right\rangle}\\\
\quad{{\left(next\coloneqq next+1\right)}^{\langle
next<N,~{}G[pos][next]\rangle}}\fatsemi\phantom{X}\\\
{\color[rgb]{.75,0,.25}\left\langle\bigoplus_{j=1}^{N}{\bigoplus_{i\in
I}}(pos=i\land next=j)^{((\mathsf{sp}_{n}^{t}(G,s,i)\land
G[i][j])+n)}\right\rangle}\\\ \quad pos\coloneqq
next\fatsemi\mathsf{assume}~{}1\\\
{\color[rgb]{.75,0,.25}\left\langle\bigoplus_{j=1}^{N}\bigoplus_{i\in
I}(pos=j)^{((\mathsf{sp}_{n}^{t}(G,s,i)\land
G[i][j])+n+1)}\right\rangle}\implies\\\
{\color[rgb]{.75,0,.25}\left\langle\bigoplus_{j=1}^{N}(pos=j)^{(\mathsf{sp}_{n+1}^{t}(G,s,j)+n+1)}\right\rangle}\\\
\end{array}$

The outcome conjunction over $i\neq t$ (corresponding to the minimum weight
path) gives us $pos=j$ with weight $\mathsf{sp}_{n+1}^{t}(G,s,j)+n+1$—it is
$n+1$ if there is path of length $n$ to some $i$ and $G[i][j]$.

The precondition is $\varphi_{0}\oplus\psi_{0}=(pos=s)$, since
$\mathsf{sp}_{0}^{t}(G,s,i)=\mathsf{false}$ when $i\neq s$ and $\mathsf{true}$
when $i=s$. Putting this all together, we get the following triple, stating
that the final position is $t$ and the weight is equal to the shortest path.

${\color[rgb]{.75,0,.25}\langle
pos=s\rangle}~{}\mathsf{SP}~{}{\color[rgb]{.75,0,.25}\langle(pos=t)^{(\mathsf{sp}(G,s,t))}\rangle}$

Note that the program does not terminate if there is no path from $s$ to $t$.
In that case, since there are no reachable outcomes, the interpretation of the
program should be $\dsser{0}$. Indeed, $\dsser{0}=\infty$ in the tropical
semiring, which is also the shortest path between two disconnected nodes. The
postcondition is therefore $(pos=t)^{(\infty)}$, meaning that the program
diverged.

##  9\. Discussion and Related Work

Computational effects have traditionally beckoned disjoint program logics
across two dimensions: different _kinds_ of effects (_e.g.,_ nondeterminism vs
randomization) and different _assertions_ about those effects (_e.g.,_ angelic
vs demonic nondeterminism). Outcome Logic (Zilberstein et al., 2023a) captures
all of those properties in a unified way, but until now the proof theory has
not been thoroughly explored.

This paper provides a relatively complete proof system for Outcome Logic,
showing that programs with effects are not only _semantically_ similar, but
also share common reasoning principles. In addition, specialized techniques
(_i.e.,_ analyzing loops with variants or invariants) are particular modes of
use of our more general framework, and are compatible with each other rather
than requiring semantically distinct program logics. This new perspective
invites increased sharing across formal methods for diverse types of programs,
and properties about those programs.

Correctness, Incorrectness, and Unified Program Logics. While formal
verification has long been the aspiration for automated static analysis, bug-
finding tools are often more practical in real engineering settings. This
partly comes down to efficiency—bugs can be found without considering all the
program traces—and partly due to the fact that most real world software just
is not correct (Distefano et al., 2019).

However, standard logical foundations of program analysis such as Hoare Logic
are prone to _false positives_ when used for bug-finding—they cannot witness
the existence of erroneous traces. In response, O’Hearn developed
Incorrectness Logic, which under-approximates the reachable states (as opposed
to Hoare Logic’s over-approximation) so as to only report bugs that truly
occur (O’Hearn, 2019).

Although Incorrectness Logic successfully serves as a logical foundation for
bug-finding tools (Raad et al., 2020; Le et al., 2022), it is semantically
incompatible with correctness analysis, making sharing of toolchains
difficult. Attention has therefore turned to ways to unify the theories of
correctness and incorrectness. This includes Exact Separation Logic, which
combines Hoare Logic and Incorrectness Logic to generate specifications that
are valid for both, but that also preludes under- or over-approximation via
the rule of consequence (Maksimović et al., 2023). Local Completeness Logic
combines Incorrectness Logic with an over-approximate abstract domain, to
similar effect (Bruni et al., 2021, 2023).

Outcome Logic. Outcome Logic unifies correctness and incorrectness reasoning
without compromising the use of logical consequences. This builds on an idea
colloquially known as _Lisbon Logic_ , first proposed by Derek Dreyer and Ralf
Jung in 2019, that has similarities to the diamond modality of Dynamic Logic
(Pratt, 1976) and Hoare’s calculus of _possible correctness_ (Hoare, 1978).
The idea was briefly mentioned in the Incorrectness Logic literature (O’Hearn,
2019; Möller et al., 2021; Le et al., 2022), but using Lisbon Logic as a
foundation of incorrectness analysis was not fully explored until the
introduction of Outcome Logic (Zilberstein et al., 2023a), which generalizes
both Lisbon Logic and Hoare Logic. The metatheory of Lisbon Logic has
subsequently been explored more deeply in a variety of unpublished manuscripts
(Ascari et al., 2023; Raad et al., 2023). Hyper Hoare Logic also generalizes
Hoare and Lisbon Logics (Dardinier and Müller, 2023), and is semantically
equivalent to the Boolean instance of OL (Example 2.4), but does not support
effects other than nondeterminism.

The initial Outcome Logic paper used a model based on both a monad and a
monoid, with looping defined via the Kleene star $C^{\star}$ (Zilberstein et
al., 2023a). The semantics of $C^{\star}$ had to be justified for each
instance. However, $C^{\star}$ is not compatible with probabilistic
computation (see Footnote 2), so an ad-hoc semantics was used in the
probabilistic case. Moreover, only the Induction rule was provided for
reasoning about $C^{\star}$, which amounts to unrolling the loop one time.
Some loops can be analyzed by applying Induction repeatedly, but it is
inadequate if the number of iterations depends at all on the program state.
Our ${C}^{\langle e,e^{\prime}\rangle}$ construct fixes this, defining
iteration in a way that supports both Kleene star
(${C}^{\langle\dsser{1},\dsser{1}\rangle}$) and also probabilistic
computation. Our Iter rule can be used to reason about any loop, even ones
that iterate an unbounded number of times.

The next Outcome Logic paper focused on a particular instance based on
separation logic (Zilberstein et al., 2023b). The model was refined to use
semirings, and the language included while loops instead of $C^{\star}$ so
that a single well-definedness proof could extend to all instances. However,
the evaluation model included additional constraints ($\dsser{1}=\top$ and
normalization) that preclude, _e.g.,_ the multiset model (Example 2.6) that we
use in this paper. Rather than giving inference rules, the paper provided a
symbolic execution algorithm, which also only supported loops via bounded
unrolling.

This paper goes beyond prior work on Outcome Logic by giving a more general
model with more instances and better support for iteration, providing a
relatively complete proof system that is able to handle any loops, and
exploring case studies related to previously unsupported types of computation
and looping.

Computational Effects. Effects have been present since the early years of
program analysis. Even basic programming languages with while loops introduce
the possibility of _nontermination_. Partial correctness was initially used to
sidestep the termination question (Floyd, 1967a; Hoare, 1969), but total
correctness (requiring termination) was later introduced too (Manna and
Pnueli, 1974). More recently, automated tools were developed to prove
(non)termination in real-world software (Berdine et al., 2006; Brockschmidt et
al., 2013; Cook et al., 2014, 2006a, 2006b; Raad et al., 2023).

Nondeterminism also showed up in early variants of Hoare Logic, stemming from
Dijkstra’s Guarded Command Language (GCL) (Dijkstra, 1975) and Dynamic Logic
(Pratt, 1976); it is useful for modeling backtracking algorithms (Floyd,
1967b) and opaque aspects of program evaluation such as user input and
concurrent scheduling. While Hoare Logic has traditionally used demonic
nondeterminism (Broy and Wirsing, 1981), other program logics have recently
arisen to deal with nondeterminism in different ways, particularly for
incorrectness (de Vries and Koutavas, 2011; O’Hearn, 2019; Möller et al.,
2021; Zilberstein et al., 2023a; Raad et al., 2023; Ascari et al., 2023).

Beginning with the seminal work of Kozen (Kozen, 1979, 1983), the study of
probabilistic programs has a rich history. This eventually led to the
development of probabilistic Hoare Logic variants (den Hartog, 2002; Barthe et
al., 2018; Rand and Zdancewic, 2015; den Hartog, 1999) that enable reasoning
about programs in terms of likelihoods and expected values. Doing so requires
pre- and postconditions to be predicates on probability distributions rather
than individual states.

Outcome Logic generalizes reasoning about all of those effects using using a
common set of inference rules. This opens up the possibility for static
analysis tools that soundly share proof fragments between different types of
programs, as shown in Section 7.

Relative Completeness and Expressivity. Any sufficiently expressive program
logic must necessarily be incomplete since, for example, the Hoare triple
${\color[rgb]{.75,0,.25}\\{\mathsf{true}\\}}~{}C~{}{\color[rgb]{.75,0,.25}\\{\mathsf{false}\\}}$
states that the program $C$ never halts, which is not provable in an axiomatic
deduction system. In response, Cook devised the idea of _relative_
completeness to convey that a proof system is adequate for analyzing a
program, but not necessarily assertions about the program states (Cook, 1978).

Expressivity requires that the assertion language used in pre- and
postconditions can describe the intermediate program states needed to, _e.g.,_
apply the Seq rule. In other words, the assertion syntax must be able to
express $\mathsf{post}(C,P)$ from Definition 4.4. Implications for an
_expressive_ language quickly become undecidable, as they must encode Peano
arithmetic (Apt, 1981; Lipton, 1977). With this in mind, the best we can hope
for is a program logic that is complete _relative_ to an oracle that decides
implications in the rule of Consequence.

The question of what an expressive (syntactic) assertion language for Outcome
Logic looks like remains open. In fact, the question of expressive assertion
languages for probabilistic Hoare Logics (which are subsumed by Outcome Logic)
is also open (den Hartog, 1999; Barthe et al., 2018). A complete probabilistic
logic with syntactic assertions does exist, but the programming language does
not include loops and is therefore considerably simplified (den Hartog, 2002);
it is unclear if this approach would extend to looping programs. To avoid the
question of expressivity, modern program logics (including our own) typically
use semantic assertions (Calcagno et al., 2007; Yang, 2001; O’Hearn, 2019;
Jung et al., 2015, 2018; Barthe et al., 2018; Kaminski, 2019; Dardinier and
Müller, 2023; Raad et al., 2023; Cousot et al., 2012; Ascari et al., 2023).
This includes logics that are mechanized within proof assistants (Barthe et
al., 2018; Jung et al., 2018, 2015; Dardinier and Müller, 2023).

Our completeness proof (Theorem 4.6) has parallels to Propositional Hoare
Logic, as we assume that axioms are available to prove properties about atomic
commands (Kozen and Tiuryn, 2001). However, in Theorem 6.1, we also show that
a particular OL instance with variable assignment is relatively complete
without additional axioms.

Quantitative Reasoning and Weighted Programming. Whereas Hoare Logic provides
a foundation for _propositional_ program analysis, quantitative program
analysis has been explored too. Probabilistic Propositional Dynamic Logic
(Kozen, 1983) and weakest pre-expectation calculi (Morgan et al., 1996;
Kaminski, 2019; Batz et al., 2019) are used to reason about randomized
programs in terms of expected values. This idea has been extended to non-
probabilistic quantitative properties too (Zhang and Kaminski, 2022; Batz et
al., 2022).

Weighted programming (Batz et al., 2022) generalizes pre-expectation reasoning
using semirings to model branch weights, much like the model of Outcome Logic
presented in this paper. Outcome Logic is a propositional analogue to weighted
programming’s quantitative model, but it is also more expressive in its
ability to reason about quantities over _multiple outcomes_. For example, in
Section 7.3, we derive a single OL triple that gives the probabilities of two
outcomes, whereas weighted programming (or weakest pre-expectations) would
need to compute each probability individually.

In the examples in Section 8 with only one outcome, OL is still more
informative—those triples not only indicate the weight of the outcome, but
also that it is the _only_ possible outcome. That is, we know that
$\mathsf{WALK}$ cannot terminate in a position other than $(N,M)$ and that
$\mathsf{SP}$ cannot terminate in a position other than $t$. With weighted
programming, there is not a straightforward way to determine the full set of
outcomes.

Finally, weighted programming cannot encode the $\Box$ and $\Diamond$
modalities from Section 3.3 and therefore cannot embed the Hoare and Lisbon
Logic reasoning principles that we showed in Section 5.

## References

  * (1)
  * Apt (1981) Krzysztof R. Apt. 1981\.  Ten Years of Hoare’s Logic: A Survey–Part I.  _ACM Trans. Program. Lang. Syst._ 3, 4 (oct 1981), 431–483.  https://doi.org/10.1145/357146.357150
  * Ascari et al. (2023) Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo. 2023.  Sufficient Incorrectness Logic: SIL and Separation SIL.  arXiv:2310.18156 [cs.LO]
  * Barthe et al. (2018) Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018.  An Assertion-Based Program Logic for Probabilistic Programs. In _Programming Languages and Systems_. Springer International Publishing, Cham, 117–144.  https://doi.org/10.1007/978-3-319-89884-1_5
  * Batz et al. (2022) Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler. 2022.  Weighted Programming: A Programming Paradigm for Specifying Mathematical Models.  _Proc. ACM Program. Lang._ 6, OOPSLA1, Article 66 (apr 2022), 30 pages.  https://doi.org/10.1145/3527310
  * Batz et al. (2019) Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019.  Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs.  _Proc. ACM Program. Lang._ 3, POPL, Article 34 (Jan 2019), 29 pages.  https://doi.org/10.1145/3290347
  * Berdine et al. (2006) Josh Berdine, Byron Cook, Dino Distefano, and Peter W. O’Hearn. 2006\.  Automatic Termination Proofs for Programs with Shape-Shifting Heaps. In _Computer Aided Verification_. Springer Berlin Heidelberg, Berlin, Heidelberg, 386–400.  https://doi.org/10.1007/11817963_35
  * Brockschmidt et al. (2013) Marc Brockschmidt, Byron Cook, and Carsten Fuhs. 2013\.  Better Termination Proving through Cooperation. In _Computer Aided Verification_. Springer Berlin Heidelberg, Berlin, Heidelberg, 413–429.  https://doi.org/10.1007/978-3-642-39799-8_28
  * Broy and Wirsing (1981) Manfred Broy and Martin Wirsing. 1981.  On the Algebraic Specification of Nondeterministic Programming Languages. In _Proceedings of the 6th Colloquium on Trees in Algebra and Programming_ _(CAAP ’81)_. Springer-Verlag, Berlin, Heidelberg, 162–179.  https://doi.org/10.5555/648216.750907
  * Bruni et al. (2021) Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. 2021.  A Logic for Locally Complete Abstract Interpretations. In _2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)_. 1–13.  https://doi.org/10.1109/LICS52264.2021.9470608
  * Bruni et al. (2023) Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. 2023.  A Correctness and Incorrectness Program Logic.  _J. ACM_ 70, 2, Article 15 (mar 2023), 45 pages.  https://doi.org/10.1145/3582267
  * Calcagno et al. (2007) Cristiano Calcagno, Peter W. O’Hearn, and Hongseok Yang. 2007\.  Local Action and Abstract Separation Logic. In _22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)_. 366–378.  https://doi.org/10.1109/LICS.2007.30
  * Cook et al. (2014) Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter O’Hearn. 2014\.  Disproving Termination with Overapproximation. In _Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design_ (Lausanne, Switzerland) _(FMCAD ’14)_. FMCAD Inc, Austin, Texas, 67–74.  https://doi.org/10.1109/FMCAD.2014.6987597
  * Cook et al. (2006a) Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006a.  Termination Proofs for Systems Code.  _SIGPLAN Not._ 41, 6 (jun 2006), 415–426.  https://doi.org/10.1145/1133255.1134029
  * Cook et al. (2006b) Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006b.  Termination Proofs for Systems Code. In _Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Ottawa, Ontario, Canada) _(PLDI ’06)_. Association for Computing Machinery, New York, NY, USA, 415–426.  https://doi.org/10.1145/1133981.1134029
  * Cook (1978) Stephen A. Cook. 1978\.  Soundness and Completeness of an Axiom System for Program Verification.  _SIAM J. Comput._ 7, 1 (feb 1978), 70–90.  https://doi.org/10.1137/0207005
  * Cousot et al. (2012) Patrick M. Cousot, Radhia Cousot, Francesco Logozzo, and Michael Barnett. 2012.  An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts. In _Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications_ (Tucson, Arizona, USA) _(OOPSLA ’12)_. Association for Computing Machinery, New York, NY, USA, 213–232.  https://doi.org/10.1145/2384616.2384633
  * Dardinier and Müller (2023) Thibault Dardinier and Peter Müller. 2023.  Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version).  https://doi.org/10.48550/ARXIV.2301.10037
  * de Vries and Koutavas (2011) Edsko de Vries and Vasileios Koutavas. 2011.  Reverse Hoare Logic. In _Software Engineering and Formal Methods_. Springer Berlin Heidelberg, Berlin, Heidelberg, 155–171.  https://doi.org/10.1007/978-3-642-24690-6_12
  * den Hartog (2002) Jerry den Hartog. 2002\.  _Probabilistic Extensions of Semantical Models_.  Ph.D. Dissertation. Vrije Universiteit Amsterdam.  https://core.ac.uk/reader/15452110
  * den Hartog (1999) J. I. den Hartog. 1999\.  Verifying Probabilistic Programs Using a Hoare like Logic. In _Advances in Computing Science — ASIAN’99_ , P. S. Thiagarajan and Roland Yap (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 113–125.
  * Dijkstra (1975) Edsger W. Dijkstra. 1975\.  Guarded Commands, Nondeterminacy and Formal Derivation of Programs.  _Commun. ACM_ 18, 8 (Aug 1975), 453–457.  https://doi.org/10.1145/360933.360975
  * Dijkstra (1976) Edsger W. Dijkstra. 1976\.  _A Discipline of Programming._ Prentice-Hall. I–XVII, 1–217 pages.
  * Dijkstra and Schölten (1990) Edsger W. Dijkstra and Carel S. Schölten. 1990.  _The strongest postcondition_.  Springer New York, New York, NY, 209–215.  https://doi.org/10.1007/978-1-4612-3228-5_12
  * Distefano et al. (2019) Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W. O’Hearn. 2019.  Scaling Static Analyses at Facebook.  _Commun. ACM_ 62, 8 (jul 2019), 62–70.  https://doi.org/10.1145/3338112
  * Docherty (2019) Simon Docherty. 2019\.  _Bunched logics: a uniform approach_.  Ph.D. Dissertation. University College London.  https://discovery.ucl.ac.uk/id/eprint/10073115/
  * Floyd (1967a) Robert W. Floyd. 1967a.  Assigning Meanings to Programs. In _Mathematical Aspects of Computer Science_ _(Proceedings of Symposia in Applied Mathematics, Vol. 19)_. American Mathematical Society, Providence, Rhode Island, 19–32.
  * Floyd (1967b) Robert W. Floyd. 1967b.  Nondeterministic Algorithms.  _J. ACM_ 14, 4 (oct 1967), 636–644.  https://doi.org/10.1145/321420.321422
  * Golan (2003) Jonathan S. Golan. 2003\.  _Semirings and Affine Equations over Them_.  Springer Dordrecht.  https://doi.org/10.1007/978-94-017-0383-3
  * Hoare (1969) C. A. R. Hoare. 1969\.  An Axiomatic Basis for Computer Programming.  _Commun. ACM_ 12, 10 (Oct. 1969), 576–580.  https://doi.org/10.1145/363235.363259
  * Hoare (1978) C. A. R. Hoare. 1978\.  Some Properties of Predicate Transformers.  _J. ACM_ 25, 3 (Jul 1978), 461–480.  https://doi.org/10.1145/322077.322088
  * Jung et al. (2018) Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2018.  Iris from the ground up: A modular foundation for higher-order concurrent separation logic.  _Journal of Functional Programming_ 28 (2018).  https://doi.org/10.1017/S0956796818000151
  * Jung et al. (2015) Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015.  Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In _Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Mumbai, India) _(POPL ’15)_. Association for Computing Machinery, New York, NY, USA, 637–650.  https://doi.org/10.1145/2676726.2676980
  * Kaminski (2019) Benjamin Lucien Kaminski. 2019\.  _Advanced weakest precondition calculi for probabilistic programs_.  Dissertation. RWTH Aachen University, Aachen.  https://doi.org/10.18154/RWTH-2019-01829
  * Karner (2004) Georg Karner. 2004\.  Continuous monoids and semirings.  _Theoretical Computer Science_ 318, 3 (2004), 355–372.  https://doi.org/10.1016/j.tcs.2004.01.020
  * Kozen (1979) Dexter Kozen. 1979\.  Semantics of probabilistic programs. In _20th Annual Symposium on Foundations of Computer Science (SFCS ’79)_. 101–114.  https://doi.org/10.1109/SFCS.1979.38
  * Kozen (1983) Dexter Kozen. 1983\.  A Probabilistic PDL. In _Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing_ _(STOC ’83)_. Association for Computing Machinery, New York, NY, USA, 291–297.  https://doi.org/10.1145/800061.808758
  * Kozen (1997) Dexter Kozen. 1997\.  Kleene Algebra with Tests.  _ACM Trans. Program. Lang. Syst._ 19, 3 (May 1997), 427–443.  https://doi.org/10.1145/256167.256195
  * Kozen and Tiuryn (2001) Dexter Kozen and Jerzy Tiuryn. 2001.  On the completeness of propositional Hoare logic.  _Information Sciences_ 139, 3 (2001), 187–195.  https://doi.org/10.1016/S0020-0255(01)00164-5 Relational Methods in Computer Science.
  * Le et al. (2022) Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022\.  Finding Real Bugs in Big Programs with Incorrectness Logic.  _Proc. ACM Program. Lang._ 6, OOPSLA1, Article 81 (Apr 2022), 27 pages.  https://doi.org/10.1145/3527325
  * Lipton (1977) Richard J. Lipton. 1977\.  A necessary and sufficient condition for the existence of hoare logics. In _18th Annual Symposium on Foundations of Computer Science (sfcs 1977)_. 1–6.  https://doi.org/10.1109/SFCS.1977.1
  * Maksimović et al. (2023) Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner. 2023.  Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. In _37th European Conference on Object-Oriented Programming (ECOOP 2023)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 263)_. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 19:1–19:27.  https://doi.org/10.4230/LIPIcs.ECOOP.2023.19
  * Manes (1976) Ernest G. Manes. 1976\.  _Algebraic Theories_.  Springer New York.  https://doi.org/10.1007/978-1-4612-9860-1
  * Manna and Pnueli (1974) Zohar Manna and Amir Pnueli. 1974.  Axiomatic Approach to Total Correctness of Programs.  _Acta Inf._ 3, 3 (sep 1974), 243–263.  https://doi.org/10.1007/BF00288637
  * Moggi (1991) Eugenio Moggi. 1991\.  Notions of computation and monads.  _Information and Computation_ 93, 1 (1991), 55–92.  https://doi.org/10.1016/0890-5401(91)90052-4
  * Möller et al. (2021) Bernhard Möller, Peter O’Hearn, and Tony Hoare. 2021\.  On Algebra of Program Correctness and & Incorrectness. In _Relational and Algebraic Methods in Computer Science: 19th International Conference, RAMiCS 2021, Marseille, France, November 2–5, 2021, Proceedings_ (Marseille, France). Springer-Verlag, Berlin, Heidelberg, 325–343.  https://doi.org/10.1007/978-3-030-88701-8_20
  * Morgan et al. (1996) Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996\.  Probabilistic Predicate Transformers.  _ACM Trans. Program. Lang. Syst._ 18, 3 (may 1996), 325–353.  https://doi.org/10.1145/229542.229547
  * O’Hearn (2019) Peter W. O’Hearn. 2019\.  Incorrectness Logic.  _Proc. ACM Program. Lang._ 4, POPL, Article 10 (Dec. 2019), 32 pages.  https://doi.org/10.1145/3371078
  * O’Hearn and Pym (1999) Peter W. O’Hearn and David J. Pym. 1999.  The Logic of Bunched Implications.  _The Bulletin of Symbolic Logic_ 5, 2 (1999), 215–244.
  * Pratt (1976) Vaughan R. Pratt. 1976\.  Semantical Considerations on Floyd-Hoare Logic. In _17th Annual Symposium on Foundations of Computer Science (sfcs 1976)_. 109–121.  https://doi.org/10.1109/SFCS.1976.27
  * Raad et al. (2020) Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O’Hearn, and Jules Villard. 2020\.  Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. In _Computer Aided Verification_. Springer International Publishing, Cham, 225–252.  https://doi.org/10.1007/978-3-030-53291-8_14
  * Raad et al. (2022) Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022.  Concurrent Incorrectness Separation Logic.  _Proc. ACM Program. Lang._ 6, POPL, Article 34 (Jan 2022), 29 pages.  https://doi.org/10.1145/3498695
  * Raad et al. (2023) Azalea Raad, Julien Vanegue, and Peter O’Hearn. 2023\.  Compositional Non-Termination Proving.  https://www.soundandcomplete.org/papers/Unter.pdf
  * Rand and Zdancewic (2015) Robert Rand and Steve Zdancewic. 2015.  VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. In _Electronic Notes in Theoretical Computer Science_ , Vol. 319. 351–367.  https://doi.org/10.1016/j.entcs.2015.12.021 The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI).
  * Różowski et al. (2023) Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. 2023\.  Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity. In _50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 261)_. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 136:1–136:20.  https://doi.org/10.4230/LIPIcs.ICALP.2023.136
  * Yang (2001) Hongseok Yang. 2001\.  _Local Reasoning for Stateful Programs_.  Ph.D. Dissertation. USA.  Advisor(s) Reddy, Uday S.  https://doi.org/10.5555/933728
  * Zhang and Kaminski (2022) Linpeng Zhang and Benjamin Lucien Kaminski. 2022.  Quantitative Strongest Post: A Calculus for Reasoning about the Flow of Quantitative Information.  _Proc. ACM Program. Lang._ 6, OOPSLA1, Article 87 (apr 2022), 29 pages.  https://doi.org/10.1145/3527331
  * Zilberstein et al. (2023a) Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023a.  Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning.  _Proc. ACM Program. Lang._ 7, OOPSLA1, Article 93 (Apr 2023), 29 pages.  https://doi.org/10.1145/3586045
  * Zilberstein et al. (2023b) Noam Zilberstein, Angelina Saliling, and Alexandra Silva. 2023b.  Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects.  (2023).  https://doi.org/10.48550/arXiv.2305.04842 arXiv:2305.04842 [cs.LO]

##  Appendix A Totality of Language Semantics

Before proving that the language semantics is total, we must first introduce a
few new concepts.

###### Definition A.1 (Natural Ordering).

Given a (partial) semiring $\langle U,+,\cdot,\dsser{0},\dsser{1}\rangle$, the
natural order is defined to be:

$u\leq v\qquad\text{iff}\qquad\exists w.~{}u+w=v$

The semiring is naturally ordered if the natural order $\leq$ is a partial
order. Note that $\leq$ is trivially reflexive and transitive, but it remains
to show that it is anti-symmetric.

Natural orders extend to weighting functions too, where $m_{1}\sqsubseteq
m_{2}$ iff there exists $m$ such that $m_{1}+m=m_{2}$. This corresponds
exactly to the pointwise order as well, so $m_{1}\sqsubseteq m_{2}$ iff
$m_{1}(\sigma)\leq m_{2}(\sigma)$ for all $\sigma\in\mathsf{supp}(m_{1})$.

###### Definition A.2 (Complete Semiring (Golan, 2003)).

A (partial) semiring $\langle U,+,\cdot,\dsser{0},\dsser{1}\rangle$ is
complete if there is a sum operator $\sum_{i\in I}$ with the following
properties:

  1. (1)

If $I=\\{i_{1},\ldots,i_{n}\\}$ is finite, then $\sum_{i\in
I}u_{i}=u_{i_{1}}+\cdots+u_{i_{n}}$

  2. (2)

If $\sum_{i\in I}x_{i}$ is defined, then $v\cdot\sum_{i\in I}u_{i}=\sum_{i\in
I}v\cdot u_{i}$ and $(\sum_{i\in I}u_{i})\cdot v=\sum_{i\in I}u_{i}\cdot v$

  3. (3)

Let $(J_{k})_{k\in K}$ be a family of nonempty disjoint subsets of $I$
($I=\bigcup_{k\in K}J_{k}$ and $J_{k}\cap J_{\ell}=\emptyset$ if $k\neq\ell$),
then $\sum_{k\in K}\sum_{j\in J_{k}}u_{j}=\sum_{i\in I}u_{i}$

###### Definition A.3 (Scott Continuity (Karner, 2004)).

A (partial) semiring with order $\leq$ is Scott Continuous if for any directed
set $D\subseteq X$ (where all pairs of elements in $D$ have a supremum), the
following hold:

$\displaystyle\sup_{x\in D}(x+y)$ $\displaystyle=(\sup D)+y$
$\displaystyle\sup_{x\in D}(x\cdot y)$ $\displaystyle=(\sup D)\cdot y$
$\displaystyle\sup_{x\in D}(y\cdot x)$ $\displaystyle=y\cdot\sup D$

###### Lemma A.4.

Let $\langle U,+,\cdot,\dsser{0},\dsser{1}\rangle$ be a complete, continuous,
naturally ordered, partial semiring. For any family of Scott continuous
functions $(f_{i}:X\to X)_{i\in I}$ and directed set $D\subseteq X$:

$\sup_{x\in D}\sum_{i\in I}f_{i}(x)=\sum_{i\in I}f_{i}(\sup D)$

###### Proof.

Since each $f_{i}$ is Scott continuous, then we know that $\\{f_{i}(x)\mid
x\in D\\}$ is a directed set. The proof proceeds by transfinite induction on
$I$.

  * $\triangleright$

Base case: $I=\\{i_{1}\\}$, then we simply need to show that $\sup_{x\in
D}f_{i_{1}}(x)=f_{i_{1}}(\sup D)$, which follows from the fact that
$f_{i_{1}}$ is Scott continuous.

  * $\triangleright$

Limit case: suppose that the claim holds for all sets smaller than $I$. It
must be possible to divide $I$ into two disjoint parts $I_{1}$ and $I_{2}$
such that $I=I_{1}\cup I_{2}$ and $I_{1}\cap I_{2}=\emptyset$. Now, given the
definition of the sum operator:

$\displaystyle\sup_{x\in D}\sum_{i\in I}f_{i}(x)$ $\displaystyle=\sup_{x\in
D}\left(\sum_{i\in I_{1}}f_{i}(x)+\sum_{i\in I_{2}}f_{i}(x)\right)$ By the
induction hypothesis, we know that $\lambda x.\sum_{i\in J}f_{i}(x)$ is Scott
continuous for any $J\subseteq I$, so given that the semiring is Scott
continuous, we can move the supremum inside the outer $+$.
$\displaystyle=(\sup_{x\in D}\sum_{i\in I_{1}}f_{i}(x))+(\sup_{x\in
D}\sum_{i\in I_{2}}f_{i}(x))$ By the induction hypothesis again:
$\displaystyle=\left(\sum_{i\in I_{1}}f_{i}(\sup D)\right)+\left(\sum_{i\in
I_{2}}f_{i}(\sup D)\right)$ $\displaystyle=\sum_{i\in I}f_{i}(\sup D)$

∎

###  A.1. Semantics of Tests and Expressions

Given some semiring $\langle U,+,\cdot,\dsser{0},\dsser{1}\rangle$, the
definition of the semantics of tests $\left\llbracket
b\right\rrbracket_{\mathsf{Test}}\colon\Sigma\to\\{\dsser{0},\dsser{1}\\}$ is
below.

$\displaystyle\left\llbracket\mathsf{true}\right\rrbracket_{\mathsf{Test}}(\sigma)$
$\displaystyle\triangleq\dsser{1}$
$\displaystyle\left\llbracket\mathsf{false}\right\rrbracket_{\mathsf{Test}}(\sigma)$
$\displaystyle\triangleq\dsser{0}$ $\displaystyle\left\llbracket b_{1}\vee
b_{2}\right\rrbracket_{\mathsf{Test}}(\sigma)$
$\displaystyle\triangleq\left\\{\begin{array}[]{ll}\dsser{1}&\text{if}~{}\left\llbracket
b_{1}\right\rrbracket_{\mathsf{Test}}(\sigma)=\dsser{1}~{}\text{or}~{}\left\llbracket
b_{2}\right\rrbracket_{\mathsf{Test}}(\sigma)=\dsser{1}\\\
\dsser{0}&\text{otherwise}\end{array}\right.$ $\displaystyle\left\llbracket
b_{1}\land b_{2}\right\rrbracket_{\mathsf{Test}}(\sigma)$
$\displaystyle\triangleq\left\\{\begin{array}[]{ll}\dsser{1}&\text{if}~{}\left\llbracket
b_{1}\right\rrbracket_{\mathsf{Test}}(\sigma)=\dsser{1}~{}\text{and}~{}\left\llbracket
b_{2}\right\rrbracket_{\mathsf{Test}}(\sigma)=\dsser{1}\\\
\dsser{0}&\text{otherwise}\end{array}\right.$
$\displaystyle\left\llbracket\lnot b\right\rrbracket_{\mathsf{Test}}(\sigma)$
$\displaystyle\triangleq\left\\{\begin{array}[]{ll}\dsser{1}&\text{if}~{}\left\llbracket
b\right\rrbracket_{\mathsf{Test}}(\sigma)=\dsser{0}\\\
\dsser{0}&\text{if}~{}\left\llbracket
b\right\rrbracket_{\mathsf{Test}}(\sigma)=\dsser{1}\end{array}\right.$
$\displaystyle\left\llbracket t\right\rrbracket_{\mathsf{Test}}(\sigma)$
$\displaystyle\triangleq\left\\{\begin{array}[]{ll}\dsser{1}&\text{if}~{}\sigma\in
t\\\ \dsser{0}&\text{if}~{}\sigma\notin t\end{array}\right.$

Based on that, we define the semantics of expressions $\left\llbracket
e\right\rrbracket\colon\Sigma\to U$.

$\displaystyle\left\llbracket b\right\rrbracket(\sigma)$
$\displaystyle\triangleq\left\llbracket
b\right\rrbracket_{\mathsf{Test}}(\sigma)$ $\displaystyle\left\llbracket
u\right\rrbracket(\sigma)$ $\displaystyle\triangleq u$

###  A.2. Fixed Point Existence

For all the proofs in this section, we assume that the operations $+$,
$\cdot$, and $\sum$ belong to a complete, Scott continuous, naturally ordered,
partial semiring with a top element (as described in Section 2.2).

###### Lemma A.5.

If $\sum_{i\in I}u_{i}$ is defined, then for any $(v_{i})_{i\in I}$,
$\sum_{i\in I}u_{i}\cdot v_{i}$ is defined.

###### Proof.

Let $v$ be the top element of $U$, so $v\geq v_{i}$ for all $i\in I$. That
means that for each $i\in I$, there is a $v_{i}^{\prime}$ such that
$v_{i}+v^{\prime}_{i}=v$. Now, since multiplication is total, then we know
that $(\sum_{i\in I}u_{i})\cdot v$ is defined. This gives us:

$(\sum_{i\in I}u_{i})\cdot v=\sum_{i\in
I}u_{i}\cdot(v_{i}+v^{\prime}_{i})=\sum_{i\in I}u_{i}\cdot v_{i}+\sum_{i\in
I}u_{i}\cdot v^{\prime}_{i}$

And since $\sum_{i\in I}u_{i}\cdot v_{i}$ is a subexpression of the above
well-defined term, then it must be well-defined. ∎

###### Lemma A.6.

For any $m\in\mathcal{W}(X)$ and $f\colon X\to\mathcal{W}(Y)$, we know that
$f^{\dagger}\colon\mathcal{W}(X)\to\mathcal{W}(Y)$ is a total function.

###### Proof.

First, recall the definition of $(-)^{\dagger}$:

$f^{\dagger}(m)(y)=\smashoperator[]{\sum_{x\in\mathsf{supp}(m)}^{}}m(x)\cdot
f(x)(y)$

To show that this is well, defined we need to show both that the sum exists,
and that the resulting weighting function has a well-defined mass. First, we
remark that since $m\in\mathcal{W}(A)$, then
$|m|=\sum_{x\in\mathsf{supp}(m)}m(x)$ must be defined. By Lemma A.5, the sum
in the definition of $(-)^{\dagger}$ is therefore defined. Now, we need to
show that $|f^{\dagger}(m)|$ is defined:

$\displaystyle|f^{\dagger}(m)|$
$\displaystyle=\smashoperator[]{\sum_{y\in\mathsf{supp}(f^{\dagger}(m))}^{}}f^{\dagger}(m)(y)$
$\displaystyle=\smashoperator[l]{\sum_{y\in\bigcup_{a\in\mathsf{supp}(m)}\mathsf{supp}(f(a))}^{}}\;\smashoperator[r]{\sum_{x\in\mathsf{supp}(m)}^{}}m(x)\cdot
f(x)(y)$ By commutativity and associativity:
$\displaystyle=\smashoperator[]{\sum_{x\in\mathsf{supp}(m)}^{}}m(x)\;\cdot\;\smashoperator[]{\sum_{y\in\mathsf{supp}(f(x))}^{}}f(x)(y)=\smashoperator[]{\sum_{x\in\mathsf{supp}(m)}^{}}m(x)\cdot|f(x)|$

Now, since $f(x)\in\mathcal{W}(Y)$ for all $x\in X$, we know that $|f(x)|$
must be defined. The outer sum also must be defined by Lemma A.5. ∎

In the following, when comparing functions $f,g\colon X\to\mathcal{W}(Y)$, we
will use the pointwise order. That is, $f\sqsubseteq g$ iff $f(x)\sqsubseteq
g(x)$ for all $x\in X$.

###### Lemma A.7.

$(-)^{\dagger}\colon(X\to\mathcal{W}(Y))\to(\mathcal{W}(X)\to\mathcal{W}(Y))$
is Scott continuous.

###### Proof.

Let $D\subseteq(X\to\mathcal{W}(Y))$ be a directed set. First, we show that
for any $x\in X$, the function $g(f)=m(x)\cdot f(x)(y)$ is Scott continuous:

$\displaystyle\sup_{f\in D}g(f)$ $\displaystyle=\sup_{f\in D}m(x)\cdot
f(x)(y)$ By Scott continuity of the $\cdot$ operator:
$\displaystyle=m(x)\cdot\sup_{f\in D}f(x)(y)$ Since we are using the pointwise
ordering: $\displaystyle=m(x)\cdot(\sup D)(x)(y)=g(\sup D)$

Now, we show that $(-)^{\dagger}$ is Scott continuous:

$\displaystyle\sup_{f\in D}f^{\dagger}$ $\displaystyle=\sup_{f\in D}\lambda
m.\smashoperator[]{\sum_{x\in\mathsf{supp}(m)}^{}}m(x)\cdot f(x)$ By Lemma
A.4, using the property we just proved. $\displaystyle=\lambda
m.\smashoperator[]{\sum_{x\in\mathsf{supp}(m)}^{}}m(x)\cdot(\sup D)(x)=(\sup
D)^{\dagger}$

∎

###### Lemma A.8.

Let $\Phi_{\langle C,e,e^{\prime}\rangle}(f)(\sigma)=\left\llbracket
e\right\rrbracket(\sigma)\cdot f^{\dagger}(\left\llbracket
C\right\rrbracket(\sigma))+\left\llbracket
e^{\prime}\right\rrbracket(\sigma)\cdot\eta(\sigma)$ and suppose that it is a
total function, then $\Phi_{\langle C,e,e^{\prime}\rangle}$ is Scott
continuous with respect to the pointwise order: $f_{1}\sqsubseteq f_{2}$ iff
$f_{1}(\sigma)\sqsubseteq f_{2}(\sigma)$ for all $\sigma\in\Sigma$.

###### Proof.

For all directed sets $D\subseteq(\Sigma\to\mathcal{W}(\Sigma))$ and
$\sigma\in\Sigma$, we have:

$\displaystyle\sup_{f\in D}\Phi_{\langle C,e,e^{\prime}\rangle}(f)(\sigma)$
$\displaystyle=\sup_{f\in D}\left(\left\llbracket
e\right\rrbracket(\sigma)\cdot f^{\dagger}(\left\llbracket
C\right\rrbracket(\sigma))+\left\llbracket
e^{\prime}\right\rrbracket(\sigma)\cdot\eta(\sigma)\right)$ By the continuity
of $+$ and $\cdot$, we can move the supremum up to the bind, which is the only
term that depends on $f$. $\displaystyle=\left\llbracket
e\right\rrbracket(\sigma)\cdot(\sup_{f\in D}f^{\dagger}(\left\llbracket
C\right\rrbracket(\sigma)))+\left\llbracket
e^{\prime}\right\rrbracket(\sigma)\cdot\eta(\sigma)$ By Lemma A.7.
$\displaystyle=\left\llbracket e\right\rrbracket(\sigma)\cdot(\sup
D)^{\dagger}(\left\llbracket C\right\rrbracket(\sigma))+\left\llbracket
e^{\prime}\right\rrbracket(\sigma)\cdot\eta(\sigma)$
$\displaystyle=\Phi_{\langle C,e,e^{\prime}\rangle}(\sup D)(\sigma)$

Since this is true for all $\sigma\in\Sigma$, $\Phi_{\langle
C,e,e^{\prime}\rangle}$ is Scott continuous. ∎

Now, given Lemma A.8 and the Kleene fixed point theorem, we know that the
least fixed point is defined and is equal to:

$\mu f.\Phi_{\langle
C,e,e^{\prime}\rangle}(f)=\sup_{n\in\mathbb{N}}\Phi^{n}_{\langle
C,e,e^{\prime}\rangle}(\lambda\tau.\dsser{0})$

Therefore the semantics of iteration loops is well-defined, assuming that
$\Phi_{\langle C,e,e^{\prime}\rangle}$ is total. In the next section, we will
see simple syntactic conditions to ensure this.

###  A.3. Syntactic Sugar

Depending on whether a partial or total semiring is used to interpret the
language semantics, unrestricted use of the $C_{1}+C_{2}$ and ${C}^{\langle
e,e^{\prime}\rangle}$ constructs may be undefined. In this section, we give
some sufficient conditions to ensure that program semantics is well-defined.
This is based on the notion of compatible expressions, introduced below.

###### Definition A.9 (Compatibility).

The expressions $e_{1}$ and $e_{2}$ are compatible in semiring
$\mathcal{A}=\langle U,+,\cdot,\dsser{0},\dsser{1}\rangle$ if $\left\llbracket
e_{1}\right\rrbracket(\sigma)+\left\llbracket e_{2}\right\rrbracket(\sigma)$
is defined for any $\sigma\in\Sigma$.

The nondeterministic (Examples 2.4 and 2.6) and tropical (Example 2.8)
instances use total semirings, so any program has well-defined semantics. In
other interpretations, we must ensure that programs are well-defined by
ensuring that all uses of choice and iteration use compatible expressions. We
begin by showing that any two collections can be combined if they are scaled
by compatible expressions.

###### Lemma A.10.

If $e_{1}$ and $e_{2}$ are compatible, then $\left\llbracket
e_{1}\right\rrbracket(\sigma)\cdot m_{1}+\left\llbracket
e_{2}\right\rrbracket(\sigma)\cdot m_{2}$ is defined for any $m_{1}$ and
$m_{2}$.

###### Proof.

Since $e_{1}$ and $e_{2}$ are compatible, then $\left\llbracket
e_{1}\right\rrbracket(\sigma)+\left\llbracket e_{2}\right\rrbracket(\sigma)$
is defined. By Lemma A.5, that also means that $\left\llbracket
e_{1}\right\rrbracket(\sigma)\cdot|m_{1}|+\left\llbracket
e_{2}\right\rrbracket(\sigma)\cdot|m_{2}|$ is defined too. Now, we have:

$\displaystyle\left\llbracket
e_{1}\right\rrbracket(\sigma)\cdot|m_{1}|+\left\llbracket
e_{2}\right\rrbracket(\sigma)\cdot|m_{2}|$ $\displaystyle=\left\llbracket
e_{1}\right\rrbracket(\sigma)\cdot\smashoperator[]{\sum_{\tau\in\mathsf{supp}(m_{1})}^{}}m_{1}(\tau)+\left\llbracket
e_{2}\right\rrbracket(\sigma)\cdot\smashoperator[]{\sum_{\tau\in\mathsf{supp}(m_{2})}^{}}m_{2}(\tau)$
$\displaystyle=\smashoperator[]{\sum_{\tau\in\mathsf{supp}(m_{1})}^{}}\left\llbracket
e_{1}\right\rrbracket(\sigma)\cdot
m_{1}(\tau)+\smashoperator[]{\sum_{\tau\in\mathsf{supp}(m_{2})}^{}}\left\llbracket
e_{2}\right\rrbracket(\sigma)\cdot m_{2}(\tau)$
$\displaystyle=\smashoperator[]{\sum_{\tau\in\mathsf{supp}(m_{1})\cup\mathsf{supp}(m_{2})}^{}}\left\llbracket
e_{1}\right\rrbracket(\sigma)\cdot m_{1}(\tau)+\left\llbracket
e_{2}\right\rrbracket(\sigma)\cdot m_{2}(\tau)$
$\displaystyle=|\left\llbracket e_{1}\right\rrbracket(\sigma)\cdot
m_{1}+\left\llbracket e_{2}\right\rrbracket(\sigma)\cdot m_{2}|$

Therefore $\left\llbracket e_{1}\right\rrbracket(\sigma)\cdot
m_{1}+\left\llbracket e_{2}\right\rrbracket(\sigma)\cdot m_{2}$ must be well-
defined. ∎

Now, we show how this result relates to program semantics. We begin with