Probabilistic Predicate Transformers

Carroll Morgan*, Annabelle McIver, Karen Seidel

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

206 Citations (Scopus)


Probabilistic predicates generalize standard predicates over a state space; with probabilistic predicate transformers one thus reasons about imperative programs in terms of probabilistic pre- and postconditions. Probabilistic healthiness conditions generalize the standard ones, characterizing "real" probabilistic programs, and are based on a connection with an underlying relational model for probabilistic execution; in both contexts demonic nondeterminism coexists with probabilistic choice. With the healthiness conditions, the associated weakest-precondition calculus seems suitable for exploring the rigorous derivation of small probabilistic programs.

Original languageEnglish
Pages (from-to)325-353
Number of pages29
JournalACM Transactions on Programming Languages and Systems
Issue number3
Publication statusPublished - May 1996
Externally publishedYes


  • D.2.4 [Program Verification]: Correctness Proofs
  • D.3.1 [Programming Languages]: Formal Definitions and Theory
  • F.1.2 [Modes of Computation]: Probabilistic Computation

Cite this