Title: A Semantics for Probabilistic Control-Flow Graphs,
Abstract: This article develops a novel operational semantics for probabilistic
control-flow graphs (pCFGs) of probabilistic imperative programs with random
assignment and "observe" (or conditioning) statements. The semantics transforms
probability distributions (on stores) as control moves from one node to another
in pCFGs. We relate this semantics to a standard, expectation-transforming,
denotational semantics of structured probabilistic imperative programs, by
translating structured programs into (unstructured) pCFGs, and proving adequacy
of the translation. This shows that the operational semantics can be used
without loss of information, and is faithful to the "intended" semantics and
hence can be used to reason about, for example, the correctness of
transformations (as we do in a companion article).