Klaus Keimel, A. Rosenbusch, Thomas Streicher. Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language. Theoretical Computer Science, 412(25):2701-2713, 2011. [doi]
Abstract is missing.