Abstract
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 language | English |
|---|---|
| Pages (from-to) | 325-353 |
| Number of pages | 29 |
| Journal | ACM Transactions on Programming Languages and Systems |
| Volume | 18 |
| Issue number | 3 |
| Publication status | Published - May 1996 |
| Externally published | Yes |
Keywords
- D.2.4 [Program Verification]: Correctness Proofs
- D.3.1 [Programming Languages]: Formal Definitions and Theory
- F.1.2 [Modes of Computation]: Probabilistic Computation