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

DOI10.1016/J.TCS.2010.12.029zbMath1226.68040OpenAlexW2013333738MaRDI 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 semanticspredicate transformersMinkowski dualityprobabilistic-nondeterministic computationweakest liberal precondition

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Related Items (3)

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

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

This page was built for publication: Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language