Correctness by construction for probabilistic programs

TL;DR

This paper introduces a correctness-by-construction approach for probabilistic programs using the probabilistic Guarded-Command Language (pGCL), enabling systematic refinement from specifications to executable code.

Contribution

It extends GCL with probabilistic choice and develops a refinement framework that preserves correctness throughout the development process.

Findings

Derived a fair-coin implementation for any discrete distribution

Algorithm for simulating a fair die close to Knuth and Yao's optimal solution

Demonstrated layered refinement steps that are independent and compositional

Abstract

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.