Annabelle McIver and Carroll Morgan
March 1996, 23pp.
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.