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

In Keimel et al. (2009) [5], we have systematically derived a predicate transformer semantics from a direct semantics in total correctness style for a nondeterministic/probabilistic basic imperative programming language Lp. In the current paper we perform the analogous task starting from a direct semantics for Lp in partial correctness style. As in [5] we establish a “Minkowski duality” providing an isomorphism between direct semantics and a continuation semantics from which a predicate transformer semantics can be read off immediately.But has only an auxiliary status and we use it to define a predicate transformer as capturing the idea of “weakest liberal preexpectation” (in analogy with weakest liberal precondition). We further explain why of while-loops is computed as a greatest fixpoint and argue why this allows one to reason about while-loops in terms of invariants as opposed to the of while-loops as considered in [5] for which this is impossible.