Developing and reasoning about probabilistic programs in pGCL

Annabelle McIver*, Carroll Morgan

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

14 Citations (Scopus)

Abstract

As explained in Chapter 1, Dijkstra's guarded-command language, which we call GCL, was introduced as an intellectual framework for rigorous reasoning about imperative sequential programs; one of its novelties was that it contained explicit "demonic" nondeterminism, representing abstraction from (or ignorance of) which of two program fragments will be executed. By introducing probabilistic nondeterminism into GCL, we provide a means with which also probabilistic programs can be rigorously developed and reasoned about. The programming logic of "weakest preconditions" for GCL becomes a logic of "greatest pre-expectations" for what we call pGCL. An expectation is a generalized predicate suitable for expressing quantitative properties such as "the probability of achieving a postcondition". pGCL is suitable for describing random algorithms, at least over discrete distributions. In our presentation of it and its logic we give a number of small examples, and two case studies. The first illustrates probabilistic "almost-certain" termination; the second case study illustrates approximated probabilities, abstraction and refinement. After a brief historical account of work on probabilistic semantics in Section 1, Section 2 gives a brief and shallow overview of pGCL, somewhat informal and concentrating on simple examples. Section 3 sets out the definitions and properties of pGCL systematically, and Section 4 treats an example of reasoning about probabilistic loops, showing how to use probabilistic invariants. Section 5 illustrates termination arguments via probabilistic variants with a thorough treatment of Rabin's choice-coordination algorithm [219]; Section 6 illustrates abstraction and refinement, as well as "approximated probabilities", by giving a two-level treatment of an almost-uniform selection algorithm. An impression of pGCL can be gained by reading Sections 2 and 4, with finally a glance over Sections 3.1 and 3.2; more thoroughly one would read Sections 2, 3.1 and 3.2, then 2 (again) and finally 4. The more theoretical Section 3.3 can be skipped on first reading. Appendix A describes basic concepts of probability theory needed in this chapter.

Original languageEnglish
Title of host publicationRefinement Techniques in Software Engineering - First Pernambuco Summer School on Software Engineering, PSSE 2004, Revised Lectures
Place of PublicationBerlin; New York
PublisherSpringer, Springer Nature
Pages123-155
Number of pages33
Volume3167 LNCS
ISBN (Electronic)9783540462545
ISBN (Print)3540462538, 9783540462538
DOIs
Publication statusPublished - 2006
Event1st Pernambuco Summer School on Software Engineering, PSSE 2004 - Recife, Brazil
Duration: 23 Nov 20045 Dec 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3167 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other1st Pernambuco Summer School on Software Engineering, PSSE 2004
CountryBrazil
CityRecife
Period23/11/045/12/04

    Fingerprint

Cite this

McIver, A., & Morgan, C. (2006). Developing and reasoning about probabilistic programs in pGCL. In Refinement Techniques in Software Engineering - First Pernambuco Summer School on Software Engineering, PSSE 2004, Revised Lectures (Vol. 3167 LNCS, pp. 123-155). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3167 LNCS). Berlin; New York: Springer, Springer Nature. https://doi.org/10.1007/11889229_4