论文标题
构造概率计划的正确性
Correctness by construction for probabilistic programs
论文作者
论文摘要
“正确的构造”范式是现代形式方法的重要组成部分，在这里，我们使用概率的守护者语言$ \ mathit {pgcl} $来说明其应用于$ \ mathit {probabilistic} $ programming。 $\mathit{pGCL}$ extends Dijkstra's guarded-command language $\mathit{GCL}$ with probabilistic choice, and is equipped with a correctness-preserving refinement relation $(\sqsubseteq)$ that enables compact, abstract specifications of probabilistic properties to be transformed gradually to concrete, executable code by applying mathematical insights in a系统和分层的方式。特征在于“构造正确性”，尽可能地，每个细化步骤层中的推理不取决于早期的层，也不影响较晚的层。我们通过得出任何给定的离散概率分布的公平实现来证明该技术。在模拟公平模拟的特殊情况下，我们的正确构造算法被证明是Knuth和Knuth和Yao的最佳解决方案的“吐痰距离”。
The "correct by construction" paradigm is an important component of modern Formal Methods, and here we use the probabilistic Guarded-Command Language $\mathit{pGCL}$ to illustrate its application to $\mathit{probabilistic}$ programming. $\mathit{pGCL}$ extends Dijkstra's guarded-command language $\mathit{GCL}$ with probabilistic choice, and is equipped with a correctness-preserving refinement relation $(\sqsubseteq)$ that enables compact, abstract specifications of probabilistic properties to be transformed gradually to concrete, executable code by applying mathematical insights in a systematic and layered way. Characteristically for "correctness by construction", as far as possible the reasoning in each refinement-step layer does not depend on earlier layers, and does not affect later ones. We demonstrate the technique by deriving a fair-coin implementation of any given discrete probability distribution. In the special case of simulating a fair die, our correct-by-construction algorithm turns out to be "within spitting distance" of Knuth and Yao's optimal solution.
