posted on 2012-10-08, 13:06authored byRiccardo Bresciani, Andrew Butterfield
We present a theory of designs based on functions from the
state space to real numbers, which we term distributions. This theory uses
predicates, in the style of UTP, based on homogeneous relations between
distributions, and is richer than the standard UTP theory of designs
as it allows us to reason about probabilistic programs; the healthiness
conditions H1{H4 of the standard theory are implicitly accounted for in
the distributional theory we present. In addition we propose a Galois
connection linkage between our distribution-based model of probabilistic
designs, and the standard UTP model of (non-probabilistic) designs.