Developing and reasoning about probabilistic programs in pGCL

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.