کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
435009 | 689850 | 2011 | 13 صفحه PDF | دانلود رایگان |
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.
Journal: Theoretical Computer Science - Volume 412, Issue 25, 3 June 2011, Pages 2701-2713