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

Authors and Affiliations

1. Department of Computer Science, Macquarie University, NSW, Australia

   Annabelle McIver

2. Department of Computer Science and Engineering, University of New South Wales, NSW, Australia

   Carroll Morgan

Editors and Affiliations

1. Department of Computer Science, University of York, York, UK

   Ana Cavalcanti

2. Centro de Informática, Universidade Federal de Pernambuco, Caixa Postal 7851, 50732-970, Recife/PE, Brazil

   Augusto Sampaio

3. University of York,  

   Jim Woodcock

Reprints and permissions

© 2006 Springer-Verlag Berlin Heidelberg

Policies and ethics