pGCL: formal reasoning for random algorithms

Abstract

Dijkstra's guarded-command language GCL contains explicit 'demonic' nondeterminism, representing abstraction from (or ignorance of ) which of two program fragments will be executed. We introduce probabilistic nondeterminism to the language, calling the result pGCL. Important is that both forms of nondeterminism are present - both demonic and probabilistic: unlike earlier approaches, we do not deal only with one or the other. The programming logic of 'weakest preconditions' for GCL becomes a logic of 'greatest pre-expectations' for pGCL: we embed predicates (Boolean-valued expressions over state variables) into arithmetic by writing [P], an expression that is 1 when P holds and 0 when it does not. Thus in a trivial sense [P] is the probability that P is true, and such embedded predicates are the basis for the more elaborate arithmetic expressions that we call "expectations". pGCL is suitable for describing random algorithms, at least over discrete distributions. In our presentation of it and its logic we give two examples: an erratic 'sequence accumulator', that fails with·some probability to move along the sequence; and Rabin's 'choice-coordination' algorithm. The first illustrates probabilistic invariants; the second illustrates probabilistic variants.