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

From MaRDI portal
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
    0 references
    0 references
    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
    0 references
    denotational semantics
    0 references
    predicate transformers
    0 references
    weakest liberal precondition
    0 references
    probabilistic-nondeterministic computation
    0 references
    Minkowski duality
    0 references

    Identifiers