Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but there is a gap when programs also exploit nondeterminism (for concurrency, efficiency, or algorithmic design). In this paper, we introduce Demonic Outcome Logic for reasoning about programs that exploit both randomization and nondeterminism. The logic includes several novel features, such as reasoning about multiple executions in tandem and manipulating pre- and postconditions using familiar equational laws -- including the distributive law of probabilistic choices over nondeterministic ones. We also give rules for loops that both establish termination and quantify the distribution of final outcomes from a single premise. We illustrate the reasoning capabilities of Demonic Outcome Logic through several case studies, including the Monty Hall problem, an adversarial protocol for simulating fair coins, and a heuristic based probabilistic SAT solver.

翻译：程序在密码学和机器学习等应用中日益依赖随机化。分析随机程序已成为一个富有成效的研究方向，但当程序同时利用非确定性（用于并发、效率或算法设计）时，存在研究空白。本文介绍了一种恶魔结果逻辑，用于推理同时利用随机化和非确定性的程序。该逻辑包含若干新颖特性，例如对多个并行执行的推理，以及使用熟悉的等式定律（包括概率选择对非确定性选择的分配律）处理前置条件和后置条件。我们还给出了循环的推理规则，这些规则既能证明终止性，又能从单一前提量化最终结果的分布。我们通过多个案例研究展示了恶魔结果逻辑的推理能力，包括蒙提霍尔问题、一个模拟公平硬币的对抗协议，以及一个基于启发式的概率SAT求解器。