Correctness by Construction for =Probabilistic= Programs

The "correct by construction” paradigm is an important

component of modern Formal Methods. This talk illustrates its purpose
and benefits by example, constructing a far-from-obvious probabilistic
program whose correctness is evident "every step of the way". That is
made possible by a correctness-preserving refinement relation (between
probabilistic/demonic program fragments) that, starting from a compact,
abstract specification, is used to construct gradually more concrete,
executable code by applying mathematical insights in a systematic and
layered style --- a style that moreover suggests to the programmer "en
route" what each construction step should be. The simple programming
language chosen is \emph{pGCL}, a probabilistic/demonic extension of
Dijkstra's language of guarded commands; and the target program
implements probabilistic choice from any given discrete distribution,
using only a series of fair-coin flips. (A final transileration from
\emph{pGCL} into Python is given, and a test run shown.)