### 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 language | English |
---|---|

Title of host publication | Refinement Techniques in Software Engineering - First Pernambuco Summer School on Software Engineering, PSSE 2004, Revised Lectures |

Place of Publication | Berlin; New York |

Publisher | Springer, Springer Nature |

Pages | 123-155 |

Number of pages | 33 |

Volume | 3167 LNCS |

ISBN (Electronic) | 9783540462545 |

ISBN (Print) | 3540462538, 9783540462538 |

DOIs | |

Publication status | Published - 2006 |

Event | 1st Pernambuco Summer School on Software Engineering, PSSE 2004 - Recife, Brazil Duration: 23 Nov 2004 → 5 Dec 2004 |

### Publication series

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

Volume | 3167 LNCS |

ISSN (Print) | 03029743 |

ISSN (Electronic) | 16113349 |

### Other

Other | 1st Pernambuco Summer School on Software Engineering, PSSE 2004 |
---|---|

Country | Brazil |

City | Recife |

Period | 23/11/04 → 5/12/04 |

### Fingerprint

### Cite this

*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