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 |
Changed an Item |
||
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 |
Revision as of 11:16, 1 July 2023
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