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

AbstractIn 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 wpa can be read off immediately.But wpa has only an auxiliary status and we use it to define a predicate transformer wlp as wlp(P)(γ)=1−wpa(P)(1−γ) capturing the idea of “weakest liberal preexpectation” (in analogy with weakest liberal precondition). We further explain why wlp 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 wp of while-loops as considered in [5] for which this is impossible