Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language (Q541217)

In this paper a predicate transformer semantics is derived from a direct semantics for a program P in a nondeterministic/probabilistic basic imperative programming language, in the case of partial correctness. The direct semantics for P is given by a function from the set S of states to the convex lower powerdomain of valuations on S. The predicate transformer semantics is obtained by establishing an isomorphism between direct semantics and a continuation semantics. But the authors are more interested in defining from this a predicate transformer wlp corresponding to the intuition of ``weakest liberal preexpectation''. They show how wlp of while-loops can be computed as a greatest fixpoint, allowing to reason about the same while-loops in terms of invariants.