The “correct by construction” paradigm is an important component of modern Formal Methods, and here we use the probabilistic Guarded-Command Language pGCL to illustrate its application to probabilistic programming.
pGCL extends Dijkstra’s guarded-command language GCL with probabilistic choice, and is equipped with a correctness-preserving refinement relation (⊆) 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.
|Title of host publication||Leveraging Applications of Formal Methods, Verification and Validation|
|Subtitle of host publication||Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings|
|Editors||Tiziana Margaria, Bernhard Steffen|
|Place of Publication||Cham, Switzerland|
|Publisher||Springer, Springer Nature|
|Number of pages||24|
|Publication status||Published - 2020|
|Event||9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020 - Rhodes, Greece|
Duration: 20 Oct 2020 → 30 Oct 2020
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Conference||9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020|
|Period||20/10/20 → 30/10/20|