Countable nondeterminism and random assignment

DOI10.1145/6490.6494zbMath0627.68015OpenAlexW2014552079MaRDI QIDQ3763571

Krzysztof R. Apt, Gordon D. Plotkin

Publication date: 1986

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/10281

zbMATH Keywords

fairnessequivalencecontinuityoperational semanticspowerdomainsnondeterminismpredicate transformerssoundness and completenesstotal correctnessweakest precondition semanticsHoare-like proof systemrecursive theoretic complexitysmall programming languagetransformation semantics

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items (49)

The origins of structural operational semantics ⋮ Merging regular processes by means of fixed-point theory ⋮ A category-theoretic semantics for unbounded indeterminacy ⋮ While-programs with nondeterministic assignments and the logic ALNA ⋮ There is no fully abstract fixpoint semantics for non-deterministic languages with infinite computations ⋮ Precise interprocedural dependence analysis of parallel programs ⋮ A complete rule for equifair termination ⋮ The weakest precondition calculus: Recursion and duality ⋮ A relation algebraic model of robust correctness ⋮ A domain equation for bisimulation ⋮ Computing polynomial program invariants ⋮ Full abstraction and recursion ⋮ A calculus of refinements for program derivations ⋮ Metric semantics for concurrency ⋮ Interpretations of recursion under unbounded nondeterminacy ⋮ A unified rule format for bounded nondeterminism in SOS with terms as labels ⋮ A methodology for designing proof rules for fair parallel programs ⋮ The \(\mu\)-calculus as an assertion-language for fairness arguments ⋮ Generated models and the ω-rule: The nondeterministic case ⋮ On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ m-Algebraic lattices in formal concept analysis ⋮ Liminf progress measures ⋮ Hiding Software Watermarks in Loop Structures ⋮ Equational reasoning about nondeterministic processes ⋮ Comparative metric semantics for concurrent PROLOG ⋮ Contractions in comparing concurrency semantics ⋮ Sequential algorithms for unbounded nondeterminism ⋮ Unnamed Item ⋮ Completing the temporal picture ⋮ An abstract interpretation-based model for safety semantics ⋮ Modelling higher-order dual nondeterminacy ⋮ On the logic of UNITY ⋮ Semantic models for total correctness and fairness ⋮ The expressive power of indeterminate dataflow primitives ⋮ ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs ⋮ A Case Study in Abstract Interpretation Based Program Transformation ⋮ Alternating states for dual nondeterminism in imperative programming ⋮ Transforming semantics by abstract interpretation ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ Fifty years of Hoare's logic ⋮ Dual unbounded nondeterminacy, recursion, and fixpoints ⋮ A logic of recursion ⋮ A fully abstract semantics for concurrent constraint programming ⋮ Ten years of Hoare's logic: A survey. II: Nondeterminism ⋮ Strong fairness and full abstraction for communicating processes ⋮ Nonexpressibility of fairness and signaling ⋮ Comparative semantics for flow of control in logic programming without logic ⋮ Soundness of data refinement for a higher-order imperative language ⋮ Constructive design of a hierarchy of semantics of a transition system by abstract interpretation

This page was built for publication: Countable nondeterminism and random assignment