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.
|Number of pages||29|
|Journal||ACM Transactions on Programming Languages and Systems|
|Publication status||Published - May 1996|
- D.2.4 [Program Verification]: Correctness Proofs
- D.3.1 [Programming Languages]: Formal Definitions and Theory
- F.1.2 [Modes of Computation]: Probabilistic Computation