Probabilistic predicate transformers: Part 2

Probabilistic predicate transformers guarantee standard (ordinary) predicate transformers to incorporate a notion of probabilistic choice in imperative programs. The basic theory of that, for finite state spaces, is set out in [5], together with a statements of their `healthiness conditions'. Here the earlier results are extended to infinite state spaces, and several more specialised topics are explored: the characterisation of standard and deterministic programs; and the structure of the extended space generated when `angelic choice' is added to the system Keywords: Probability, predicate transformers, non-determinism, verification, refinement, imperative programming, program derivation, Galois connection. 1 Introduction Probabilistic predicate transformers were introduced originally in Kozen ([4]) as a framework for reasoning about imperative probabilistic programs. In [5] we extend that earlier work to include (demonic) nondeterminism, thus placing it on a par with the general tre..