Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language (Q541217): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(6 intermediate revisions by 5 users not shown) | |||
Property / author | |||
Property / author: Klaus Keimel / rank | |||
Property / author | |||
Property / author: Thomas Streicher / rank | |||
Property / author | |||
Property / author: Klaus Keimel / rank | |||
Normal rank | |||
Property / author | |||
Property / author: Thomas Streicher / rank | |||
Normal rank | |||
Property / review text | |||
In this paper a predicate transformer semantics is derived from a direct semantics for a program P in a nondeterministic/probabilistic basic imperative programming language, in the case of partial correctness. The direct semantics for P is given by a function from the set S of states to the convex lower powerdomain of valuations on S. The predicate transformer semantics is obtained by establishing an isomorphism between direct semantics and a continuation semantics. But the authors are more interested in defining from this a predicate transformer wlp corresponding to the intuition of ``weakest liberal preexpectation''. They show how wlp of while-loops can be computed as a greatest fixpoint, allowing to reason about the same while-loops in terms of invariants. | |||
Property / review text: In this paper a predicate transformer semantics is derived from a direct semantics for a program P in a nondeterministic/probabilistic basic imperative programming language, in the case of partial correctness. The direct semantics for P is given by a function from the set S of states to the convex lower powerdomain of valuations on S. The predicate transformer semantics is obtained by establishing an isomorphism between direct semantics and a continuation semantics. But the authors are more interested in defining from this a predicate transformer wlp corresponding to the intuition of ``weakest liberal preexpectation''. They show how wlp of while-loops can be computed as a greatest fixpoint, allowing to reason about the same while-loops in terms of invariants. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Anna Labella / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q55 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B70 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 5904441 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
denotational semantics | |||
Property / zbMATH Keywords: denotational semantics / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
predicate transformers | |||
Property / zbMATH Keywords: predicate transformers / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
weakest liberal precondition | |||
Property / zbMATH Keywords: weakest liberal precondition / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
probabilistic-nondeterministic computation | |||
Property / zbMATH Keywords: probabilistic-nondeterministic computation / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
Minkowski duality | |||
Property / zbMATH Keywords: Minkowski duality / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.tcs.2010.12.029 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2013333738 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4813222 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Continuous Lattices and Domains / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Predicate transformers for extended probability and non-determinism / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Partial correctness for probabilistic demonic programs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Abstraction, Refinement and Proof for Probabilistic Systems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Domain-Theoretic Foundations of Functional Programming / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Semantic domains for combining probability and non-determinism / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 03:52, 4 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language |
scientific article |
Statements
Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language (English)
0 references
6 June 2011
0 references
In this paper a predicate transformer semantics is derived from a direct semantics for a program P in a nondeterministic/probabilistic basic imperative programming language, in the case of partial correctness. The direct semantics for P is given by a function from the set S of states to the convex lower powerdomain of valuations on S. The predicate transformer semantics is obtained by establishing an isomorphism between direct semantics and a continuation semantics. But the authors are more interested in defining from this a predicate transformer wlp corresponding to the intuition of ``weakest liberal preexpectation''. They show how wlp of while-loops can be computed as a greatest fixpoint, allowing to reason about the same while-loops in terms of invariants.
0 references
denotational semantics
0 references
predicate transformers
0 references
weakest liberal precondition
0 references
probabilistic-nondeterministic computation
0 references
Minkowski duality
0 references