Correctness by construction for probabilistic programs

Annabelle McIver; Carroll Morgan

doi:10.1007/978-3-030-61362-4_12

Correctness by construction for probabilistic programs

Annabelle McIver^*, Carroll Morgan

^*Corresponding author for this work

School of Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

7 Citations (Scopus)

Abstract

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.

Original language	English
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
Pages	216-239
Number of pages	24
ISBN (Electronic)	9783030613624
ISBN (Print)	9783030613617
DOIs	https://doi.org/10.1007/978-3-030-61362-4_12
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

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12476 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020
Country/Territory	Greece
City	Rhodes
Period	20/10/20 → 30/10/20

Access to Document

10.1007/978-3-030-61362-4_12

Cite this

McIver, A., & Morgan, C. (2020). Correctness by construction for probabilistic programs. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings (pp. 216-239). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12476 LNCS). Springer, Springer Nature. https://doi.org/10.1007/978-3-030-61362-4_12

McIver, Annabelle ; Morgan, Carroll. / Correctness by construction for probabilistic programs. Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. editor / Tiziana Margaria ; Bernhard Steffen. Cham, Switzerland : Springer, Springer Nature, 2020. pp. 216-239 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ad1540c20e714b0dbb36e08da73b4a4f,

title = "Correctness by construction for probabilistic programs",

abstract = "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{\textquoteright}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{\textquoteright}s optimal solution.",

author = "Annabelle McIver and Carroll Morgan",

year = "2020",

doi = "10.1007/978-3-030-61362-4_12",

language = "English",

isbn = "9783030613617",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer, Springer Nature",

pages = "216--239",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation",

address = "United States",

note = "9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020 ; Conference date: 20-10-2020 Through 30-10-2020",

}

McIver, A & Morgan, C 2020, Correctness by construction for probabilistic programs. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12476 LNCS, Springer, Springer Nature, Cham, Switzerland, pp. 216-239, 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020, Rhodes, Greece, 20/10/20. https://doi.org/10.1007/978-3-030-61362-4_12

Correctness by construction for probabilistic programs. / McIver, Annabelle; Morgan, Carroll.
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. ed. / Tiziana Margaria; Bernhard Steffen. Cham, Switzerland: Springer, Springer Nature, 2020. p. 216-239 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12476 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Correctness by construction for probabilistic programs

AU - McIver, Annabelle

AU - Morgan, Carroll

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85097376148&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-61362-4_12

DO - 10.1007/978-3-030-61362-4_12

M3 - Conference proceeding contribution

AN - SCOPUS:85097376148

SN - 9783030613617

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 216

EP - 239

BT - Leveraging Applications of Formal Methods, Verification and Validation

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer, Springer Nature

CY - Cham, Switzerland

T2 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020

Y2 - 20 October 2020 through 30 October 2020

ER -

McIver A, Morgan C. Correctness by construction for probabilistic programs. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. Cham, Switzerland: Springer, Springer Nature. 2020. p. 216-239. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-61362-4_12

Correctness by construction for probabilistic programs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this