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

DOI10.1016/j.tcs.2010.12.029zbMath1226.68040MaRDI QIDQ541217

A. Rosenbusch, Klaus Keimel, Thomas Streicher

Publication date: 6 June 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2010.12.029

zbMATH Keywords

denotational semantics; predicate transformers; Minkowski duality; probabilistic-nondeterministic computation; weakest liberal precondition

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q55: Semantics in the theory of computing

Related Items

Healthiness conditions for predicate transformers, The expectation monad in quantum foundations, Generic weakest precondition semantics from monads enriched with order

Cites Work

• Unnamed Item
• Semantic domains for combining probability and non-determinism
• A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language
• Domain-Theoretic Foundations of Functional Programming
• Predicate transformers for extended probability and non-determinism
• Abstraction, Refinement and Proof for Probabilistic Systems
• Continuous Lattices and Domains
• Partial correctness for probabilistic demonic programs